ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>hχ₁ : χ₁ ≠ 0<GOAL>∀ᶠ (k : ℕ) in Filter.atTop, LieModule.weightSpace M (k • χ₁ + χ₂) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>hχ₁ : χ₁ ≠ 0<GOAL>∃ k > 0, LieModule.weightSpace M (k • χ₁ + χ₂) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>hχ₁ : χ₁ ≠ 0<GOAL>∃ p < 0, ∃ q > 0, LieModule.weightSpace M (p • χ₁ + χ₂) = ⊥ ∧ LieModule.weightSpace M (q • χ₁ + χ₂) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<GOAL>LieModule.weightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Set.Ioo p q, LieModule.weightSpace M (k • χ₁ + χ₂)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<GOAL>LieModule.weightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, LieModule.weightSpace M (k • χ₁ + χ₂)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<GOAL>LieModule.weightSpaceChain M (-χ₁) χ₂ (-q) (-p) = LieModule.weightSpaceChain M χ₁ χ₂ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<VAR>k : ℤ<VAR>hk : k ∈ Set.Ioo p q<GOAL>LieModule.weightSpace M (k • χ₁ + χ₂) ≤ LieModule.weightSpaceChain M χ₁ χ₂ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>hq : LieModule.weightSpace M (q • α + χ) = ⊥<VAR>x : L<VAR>hx : x ∈ LieAlgebra.rootSpace H α<VAR>y : M<VAR>hy : y ∈ LieModule.weightSpaceChain M α χ p q<GOAL>⁅x, y⁆ ∈ LieModule.weightSpaceChain M α χ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>hp : LieModule.weightSpace M (p • α + χ) = ⊥<VAR>x : L<VAR>hx : x ∈ LieAlgebra.rootSpace H (-α)<VAR>y : M<VAR>hy : y ∈ LieModule.weightSpaceChain M α χ p q<GOAL>⁅x, y⁆ ∈ LieModule.weightSpaceChain M α χ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>H.IsCartanSubalgebra<VAR>IsNoetherian R L<VAR>hp : LieModule.weightSpace M (p • α + χ) = ⊥<VAR>hq : LieModule.weightSpace M (q • α + χ) = ⊥<VAR>x : ↥H<VAR>hx : x ∈ LieAlgebra.corootSpace α<GOAL>(LinearMap.trace R ↥↑(LieModule.weightSpaceChain M α χ p q)) ((LieModule.toEnd R ↥H ↥↑(LieModule.weightSpaceChain M α χ p q)) x) = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>H.IsCartanSubalgebra<VAR>IsNoetherian R L<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>CharZero R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : LieModule.weightSpace M χ ≠ ⊥<GOAL>∃ a b, 0 < b ∧ ∀ x ∈ LieAlgebra.corootSpace α, (a • α + b • χ) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<GOAL>LieModule.chainTopCoeff (-α) β = LieModule.chainBotCoeff α β
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<GOAL>LieModule.chainBotCoeff (-α) β = LieModule.chainTopCoeff α β
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>β : LieModule.Weight R L M<GOAL>LieModule.chainTopCoeff 0 β = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>β : LieModule.Weight R L M<GOAL>LieModule.chainBotCoeff 0 β = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<VAR>hα : α ≠ 0<GOAL>LieModule.chainTopCoeff α β + 1 = Nat.find ⋯
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<VAR>hα : α ≠ 0<GOAL>LieModule.weightSpace M ((LieModule.chainTopCoeff α β + 1) • α + ⇑β) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<VAR>hα : α ≠ 0<GOAL>LieModule.weightSpace M ((↑(LieModule.chainTopCoeff α β) + 1) • α + ⇑β) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<VAR>n : ℕ<VAR>hn : n ≤ LieModule.chainTopCoeff α β<GOAL>LieModule.weightSpace M (n • α + ⇑β) ≠ ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<VAR>hα : α ≠ 0<GOAL>LieModule.weightSpace M ((-↑(LieModule.chainBotCoeff α β) - 1) • α + ⇑β) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<VAR>n : ℤ<VAR>hn : -↑(LieModule.chainBotCoeff α β) ≤ n<VAR>hn' : n ≤ ↑(LieModule.chainTopCoeff α β)<GOAL>LieModule.weightSpace M (n • α + ⇑β) ≠ ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<VAR>n : ℕ<VAR>hn : n ≤ LieModule.chainBotCoeff α β<GOAL>LieModule.weightSpace M (-↑n • α + ⇑β) ≠ ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<GOAL>⇑(LieModule.chainTop α β) = LieModule.chainTopCoeff α β • α + ⇑β
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<GOAL>⇑(LieModule.chainTop α β) = ↑(LieModule.chainTopCoeff α β) • α + ⇑β
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<GOAL>⇑(LieModule.chainBot α β) = -↑(LieModule.chainBotCoeff α β) • α + ⇑β
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<GOAL>LieModule.chainTop (-α) β = LieModule.chainBot α β
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<GOAL>LieModule.chainBot (-α) β = LieModule.chainTop α β
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>β : LieModule.Weight R L M<GOAL>LieModule.chainTop 0 β = β
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>β : LieModule.Weight R L M<GOAL>LieModule.chainBot 0 β = β
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<VAR>hα : α ≠ 0<GOAL>LieModule.weightSpace M (α + ⇑(LieModule.chainTop α β)) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<VAR>hα : α ≠ 0<GOAL>LieModule.weightSpace M (-α + ⇑(LieModule.chainBot α β)) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α : L → R<VAR>β : LieModule.Weight R L M<VAR>hα : α ≠ 0<VAR>hα' : LieModule.weightSpace M α ≠ ⊥<GOAL>(LieModule.chainTop α β).IsNonZero
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>NoZeroSMulDivisors ℤ R<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>α β : LieModule.Weight R L M<VAR>hα : α.IsNonZero<GOAL>(LieModule.chainTop (⇑α) β).IsNonZero
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x y : L<GOAL>((LieModule.traceForm R L M) x) y = (LinearMap.trace R M) (φ x ∘ₗ φ y)
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x y : L<GOAL>((LieModule.traceForm R L M) x) y = ((LieModule.traceForm R L M) y) x
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<GOAL>LinearMap.IsSymm (LieModule.traceForm R L M)
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<GOAL>LinearMap.flip (LieModule.traceForm R L M) = LieModule.traceForm R L M
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x y z : L<GOAL>((LieModule.traceForm R L M) ⁅x, y⁆) z = ((LieModule.traceForm R L M) x) ⁅y, z⁆
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x y z : L<GOAL>((LieModule.traceForm R L M) ⁅x, y⁆) z = -((LieModule.traceForm R L M) y) ⁅x, z⁆
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<GOAL>LinearMap.BilinForm.lieInvariant L (LieModule.traceForm R L M)
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x : L<GOAL>⁅x, LieModule.traceForm R L M⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>IsReduced R<VAR>LieModule.IsNilpotent R L M<GOAL>LieModule.traceForm R L M = 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>LieAlgebra.IsNilpotent R L<VAR>IsNoetherian R M<VAR>LieModule.LinearWeights R L M<VAR>χ : L → R<VAR>x y : L<GOAL>((LieModule.traceForm R L ↥↑(LieModule.weightSpace M χ)) x) y = FiniteDimensional.finrank R ↥↑(LieModule.weightSpace M χ) • (χ x * χ y)
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x y : L<VAR>k : ℕ<VAR>hx : x ∈ ⊤.lcs L k<VAR>hy : y ∈ LieSubmodule.ucs k ⊥<GOAL>((LieModule.traceForm R L M) x) y = 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x y : L<VAR>hx : x ∈ LieModule.lowerCentralSeries R L L 1<VAR>hy : y ∈ LieAlgebra.center R L<GOAL>((LieModule.traceForm R L M) x) y = 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieModule.IsTrivial L M<GOAL>LieModule.traceForm R L M = 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieAlgebra.IsNilpotent R L<VAR>B : LinearMap.BilinForm R M<VAR>hB : ∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆<VAR>m₀ m₁ : M<VAR>hm₀ : m₀ ∈ LieModule.weightSpace M 0<VAR>hm₁ : m₁ ∈ LieModule.posFittingComp R L M<GOAL>(B m₀) m₁ = 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>k : ℕ<VAR>x : L<VAR>hk : 1 ≤ k<VAR>hx : x ∈ LieModule.lowerCentralSeries R L L k<GOAL>(LinearMap.trace R M) (φ x) = 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>L' : LieSubalgebra R L<VAR>x : L<VAR>hx : x ∈ L'<VAR>y : ↥L'<GOAL>((LieModule.traceForm R (↥L') M) ⟨x, hx⟩) y = ((LieModule.traceForm R L M) x) ↑y
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>L' : LieSubalgebra R L<VAR>x : ↥L'<VAR>y : L<VAR>hy : y ∈ L'<GOAL>((LieModule.traceForm R (↥L') M) x) ⟨y, hy⟩ = ((LieModule.traceForm R L M) ↑x) y
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>LieAlgebra.IsNilpotent R L<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>LieModule.IsTriangularizable R L M<VAR>z : L<GOAL>LieModule.traceForm R L M = ∑ χ ∈ ⋯.toFinset, LieModule.traceForm R L ↥↑(LieModule.weightSpaceOf M χ z)
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>LieAlgebra.IsNilpotent R L<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<GOAL>(lieIdealSubalgebra R L (LieModule.lowerCentralSeries R L L 1 ⊓ LieAlgebra.center R L)).toSubmodule ≤ LinearMap.ker (LieModule.traceForm R L M)
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>LieAlgebra.IsNilpotent R L<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>h : LinearMap.ker (LieModule.traceForm R L M) = ⊥<GOAL>IsLieAbelian L
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<VAR>x : L<VAR>y : L<VAR>hy : y ∈ I<VAR>hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N := ⋯<GOAL>(LinearMap.trace R M) (φ x ∘ₗ φ y) = (LinearMap.trace R ↥↑N) ((φ x ∘ₗ φ y).restrict hy')
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<GOAL>LieModule.traceForm R ↥↑I ↥↑N = (LieModule.traceForm R L M).restrict (lieIdealSubalgebra R L I).toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<VAR>x : L<VAR>y : L<VAR>hy : y ∈ I<VAR>LieModule.IsTrivial ↥↑I ↥↑N<GOAL>(LinearMap.trace R M) (φ x ∘ₗ φ y) = 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x y : L<GOAL>((killingForm R L) x) y = (LinearMap.trace R L) ((LieAlgebra.ad R L) x ∘ₗ (LieAlgebra.ad R L) y)
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>x₀ x₁ : L<VAR>hx₀ : x₀ ∈ LieAlgebra.zeroRootSubalgebra R L H<VAR>hx₁ : x₁ ∈ LieModule.posFittingComp R (↥H) L<GOAL>((killingForm R L) x₀) x₁ = 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>↑(LieIdeal.killingCompl R L I) = (killingForm R L).orthogonal ↑I
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>x : L<GOAL>x ∈ LieIdeal.killingCompl R L I ↔ ∀ y ∈ I, ((killingForm R L) y) x = 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>(lieIdealSubalgebra R L (LieIdeal.killingCompl R L ⊤)).toSubmodule = LinearMap.ker (killingForm R L)
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Free R L<VAR>Module.Finite R L<VAR>I : LieIdeal R L<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<GOAL>killingForm R ↥↑I = (killingForm R L).restrict (lieIdealSubalgebra R L I).toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>(killingForm R L).restrict (lieIdealSubalgebra R L I).toSubmodule = LieModule.traceForm R (↥↑I) L
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Free R L<VAR>Module.Finite R L<VAR>I : LieIdeal R L<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>IsLieAbelian ↥↑I<GOAL>I ≤ LieIdeal.killingCompl R L ⊤
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>Field K<VAR>LieAlgebra K L<VAR>Module K M<VAR>LieModule K L M<VAR>FiniteDimensional K M<VAR>LieAlgebra.IsNilpotent K L<VAR>LieModule.LinearWeights K L M<VAR>LieModule.IsTriangularizable K L M<VAR>x y : L<GOAL>((LieModule.traceForm K L M) x) y = ∑ χ : LieModule.Weight K L M, FiniteDimensional.finrank K ↥↑(LieModule.weightSpace M ⇑χ) • (χ x * χ y)
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>Field K<VAR>LieAlgebra K L<VAR>Module K M<VAR>LieModule K L M<VAR>FiniteDimensional K M<VAR>LieAlgebra.IsNilpotent K L<VAR>LieModule.LinearWeights K L M<VAR>LieModule.IsTriangularizable K L M<GOAL>LieModule.traceForm K L M = ∑ χ : LieModule.Weight K L M, FiniteDimensional.finrank K ↥↑(LieModule.weightSpace M ⇑χ) • (LieModule.Weight.toLinear K L M χ).smulRight (LieModule.Weight.toLinear K L M χ)
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>Field K<VAR>LieAlgebra K L<VAR>Module K M<VAR>LieModule K L M<VAR>FiniteDimensional K M<VAR>LieAlgebra.IsNilpotent K L<VAR>LieModule.LinearWeights K L M<VAR>LieModule.IsTriangularizable K L M<GOAL>LinearMap.range (LieModule.traceForm K L M) ≤ Submodule.span K (Set.range (LieModule.Weight.toLinear K L M))
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑(MulOpposite.opLinearEquiv R) = MulOpposite.op
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑(MulOpposite.opLinearEquiv R).symm = MulOpposite.unop