ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>M₂ : Type u_5<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : Function.Injective ⇑f<GOAL>LieSubmodule.comap f (LieModule.weightSpace M₂ χ) = LieModule.weightSpace M χ
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>M₂ : Type u_5<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : Function.Injective ⇑f<GOAL>LieSubmodule.map f (LieModule.weightSpace M χ) = LieModule.weightSpace M₂ χ ⊓ f.range
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>M₂ : Type u_5<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>χ : L → R<VAR>e : M ≃ₗ⁅R,L⁆ M₂<GOAL>LieSubmodule.map e.toLieModuleHom (LieModule.weightSpace M χ) = LieModule.weightSpace M₂ χ
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>M₂ : Type u_5<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>e : M ≃ₗ⁅R,L⁆ M₂<GOAL>LieSubmodule.map e.toLieModuleHom (LieModule.posFittingComp R L M) = LieModule.posFittingComp R L M₂
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsNoetherian R M<VAR>IsArtinian R M<VAR>N₁ N₂ : LieSubmodule R L M<VAR>h : Codisjoint N₁ N₂<GOAL>LieSubmodule.map N₁.incl (LieModule.posFittingComp R L ↥↑N₁) ⊔ LieSubmodule.map N₂.incl (LieModule.posFittingComp R L ↥↑N₂) = LieModule.posFittingComp R L M
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x : L<VAR>χ : L → R<GOAL>LieSubmodule.map (LieModule.weightSpaceOf M (χ x) x).incl (LieModule.weightSpace (↥↑(LieModule.weightSpaceOf M (χ x) x)) χ) = LieModule.weightSpace M χ
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsNoetherian R M<VAR>IsArtinian R M<VAR>x : L<GOAL>IsCompl (LieModule.weightSpaceOf M 0 x) (LieModule.posFittingCompOf R M x)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsNoetherian R M<VAR>IsArtinian R M<VAR>h : ∀ N < ⊤, IsCompl (LieModule.weightSpace (↥↑N) 0) (LieModule.posFittingComp R L ↥↑N)<GOAL>IsCompl (LieModule.weightSpace M 0) (LieModule.posFittingComp R L M)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsNoetherian R M<VAR>IsArtinian R M<GOAL>IsCompl (LieModule.weightSpace M 0) (LieModule.posFittingComp R L M)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>NoZeroSMulDivisors R M<VAR>x : L<VAR>φ₁ φ₂ : R<VAR>h : φ₁ ≠ φ₂<GOAL>Disjoint (LieModule.weightSpaceOf M φ₁ x) (LieModule.weightSpaceOf M φ₂ x)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>NoZeroSMulDivisors R M<VAR>χ₁ χ₂ : L → R<VAR>h : χ₁ ≠ χ₂<GOAL>Disjoint (LieModule.weightSpace M χ₁) (LieModule.weightSpace M χ₂)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>NoZeroSMulDivisors R M<GOAL>Set.InjOn (fun χ => LieModule.weightSpace M χ) {χ | LieModule.weightSpace M χ ≠ ⊥}
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>NoZeroSMulDivisors R M<GOAL>CompleteLattice.Independent fun χ => LieModule.weightSpace M χ
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>NoZeroSMulDivisors R M<GOAL>CompleteLattice.Independent fun χ => LieModule.weightSpace M ⇑χ
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>NoZeroSMulDivisors R M<VAR>x : L<GOAL>CompleteLattice.Independent fun χ => LieModule.weightSpaceOf M χ x
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<VAR>x : L<GOAL>{χ | LieModule.weightSpaceOf M χ x ≠ ⊥}.Finite
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>NoZeroSMulDivisors R M<VAR>IsNoetherian R M<GOAL>{χ | LieModule.weightSpace M χ ≠ ⊥}.Finite
<VAR>R : Type u_2<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>self : LieModule.IsTriangularizable R L M<VAR>x : L<GOAL>⨆ φ, ⨆ k, (((LieModule.toEnd R L M) x).genEigenspace φ) k = ⊤
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieModule.IsTriangularizable R L M<VAR>x : L<GOAL>⨆ φ, LieModule.weightSpaceOf M φ x = ⊤
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>χ : L → R<VAR>x : L<GOAL>(LinearMap.trace R ↥↑(LieModule.weightSpace M χ)) ((LieModule.toEnd R L ↥↑(LieModule.weightSpace M χ)) x) = FiniteDimensional.finrank R ↥↑(LieModule.weightSpace M χ) • χ x
<VAR>K : Type u_1<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>LieAlgebra.IsNilpotent K L<VAR>FiniteDimensional K M<VAR>LieModule.IsTriangularizable K L M<GOAL>⨆ χ, LieModule.weightSpace M χ = ⊤
<VAR>K : Type u_1<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>LieAlgebra.IsNilpotent K L<VAR>FiniteDimensional K M<VAR>LieModule.IsTriangularizable K L M<GOAL>⨆ χ, LieModule.weightSpace M ⇑χ = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>CommSemiring R<VAR>CommSemiring S<VAR>x : S<VAR>f : R →+* Polynomial S<VAR>g : σ → Polynomial S<VAR>p : MvPolynomial σ R<GOAL>Polynomial.eval x (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) p
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x : Fin n → R<VAR>CommSemiring R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>q : MvPolynomial (Fin n) R<GOAL>(MvPolynomial.eval x) (Polynomial.eval q ((MvPolynomial.finSuccEquiv R n) f)) = (MvPolynomial.eval fun i => Fin.cases ((MvPolynomial.eval x) q) x i) f
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Algebra R S<VAR>Module S N<VAR>IsScalarTower R S N<VAR>p : Submonoid R<VAR>IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>IsLocalizedModule p f<VAR>M' : Submodule R M<VAR>x : N<GOAL>x ∈ Submodule.localized' S p f M' ↔ ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Algebra R S<VAR>Module S N<VAR>IsScalarTower R S N<VAR>p : Submonoid R<VAR>IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>IsLocalizedModule p f<VAR>M' : Submodule R M<VAR>c : ↥M'<GOAL>↑((Submodule.toLocalized' S p f M') c) = f ↑c
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Algebra R S<VAR>Module S N<VAR>IsScalarTower R S N<VAR>p : Submonoid R<VAR>IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>IsLocalizedModule p f<VAR>M' : Submodule R M<VAR>x : M<GOAL>(Submodule.toLocalizedQuotient' S p f M') (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Algebra R S<VAR>Module S N<VAR>IsScalarTower R S N<VAR>p : Submonoid R<VAR>IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>IsLocalizedModule p f<VAR>P : Type w<VAR>AddCommGroup P<VAR>Module R P<VAR>Q : Type w'<VAR>AddCommGroup Q<VAR>Module R Q<VAR>Module S Q<VAR>IsScalarTower R S Q<VAR>f' : P →ₗ[R] Q<VAR>IsLocalizedModule p f'<VAR>g : M →ₗ[R] P<GOAL>Submodule.localized' S p f (LinearMap.ker g) = LinearMap.ker (LinearMap.extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g))
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Algebra R S<VAR>Module S N<VAR>IsScalarTower R S N<VAR>p : Submonoid R<VAR>IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>IsLocalizedModule p f<VAR>P : Type w<VAR>AddCommGroup P<VAR>Module R P<VAR>Q : Type w'<VAR>AddCommGroup Q<VAR>Module R Q<VAR>Module S Q<VAR>IsScalarTower R S Q<VAR>f' : P →ₗ[R] Q<VAR>IsLocalizedModule p f'<VAR>g : M →ₗ[R] P<GOAL>LinearMap.ker ((IsLocalizedModule.map p f f') g) = Submodule.restrictScalars R (Submodule.localized' S p f (LinearMap.ker g))
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type v'<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>p : Submonoid R<VAR>f : M →ₗ[R] N<VAR>IsLocalizedModule p f<VAR>P : Type w<VAR>AddCommGroup P<VAR>Module R P<VAR>Q : Type w'<VAR>AddCommGroup Q<VAR>Module R Q<VAR>f' : P →ₗ[R] Q<VAR>IsLocalizedModule p f'<VAR>g : M →ₗ[R] P<VAR>c : ↥(LinearMap.ker g)<GOAL>↑((LinearMap.toKerIsLocalized p f f' g) c) = f ↑c
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Algebra R S<VAR>Module S N<VAR>IsScalarTower R S N<VAR>p : Submonoid R<VAR>IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>IsLocalizedModule p f<VAR>P : Type w<VAR>AddCommGroup P<VAR>Module R P<VAR>Q : Type w'<VAR>AddCommGroup Q<VAR>Module R Q<VAR>Module S Q<VAR>IsScalarTower R S Q<VAR>f' : P →ₗ[R] Q<VAR>IsLocalizedModule p f'<VAR>g : M →ₗ[R] P<GOAL>IsLocalizedModule p (LinearMap.toKerIsLocalized p f f' g)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>x : L<VAR>hx : x ∈ LieAlgebra.rootSpace H ⇑(LieModule.chainTop (⇑α) β)<GOAL>∃ n, n • x = ⁅LieAlgebra.IsKilling.coroot α, x⁆
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hα : α.IsZero<GOAL>LieAlgebra.IsKilling.chainLength α β = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>x : L<VAR>hx : x ∈ LieAlgebra.rootSpace H ⇑(LieModule.chainTop (⇑α) β)<GOAL>LieAlgebra.IsKilling.chainLength α β • x = ⁅LieAlgebra.IsKilling.coroot α, x⁆
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>x : L<VAR>hx : x ∈ LieAlgebra.rootSpace H ⇑(LieModule.chainTop (⇑α) β)<GOAL>↑(LieAlgebra.IsKilling.chainLength α β) • x = ⁅LieAlgebra.IsKilling.coroot α, x⁆
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<GOAL>β (LieAlgebra.IsKilling.coroot α) = ↑(↑(LieAlgebra.IsKilling.chainLength α β) - 2 * ↑(LieModule.chainTopCoeff (⇑α) β))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>n : ℕ<VAR>hn : n ≤ LieAlgebra.IsKilling.chainLength α β<GOAL>LieAlgebra.rootSpace H (-(n • ⇑α) + ⇑(LieModule.chainTop (⇑α) β)) ≠ ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : LieAlgebra.IsKilling.chainLength α β < n<GOAL>LieAlgebra.rootSpace H (-(n • ⇑α) + ⇑(LieModule.chainTop (⇑α) β)) = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<GOAL>LieModule.chainTopCoeff (⇑α) β ≤ LieAlgebra.IsKilling.chainLength α β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<GOAL>LieModule.chainBotCoeff (⇑α) β + LieModule.chainTopCoeff (⇑α) β = LieAlgebra.IsKilling.chainLength α β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<GOAL>LieModule.chainTopCoeff (⇑α) β + LieModule.chainBotCoeff (⇑α) β = LieAlgebra.IsKilling.chainLength α β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<GOAL>LieModule.chainBotCoeff (⇑α) β ≤ LieAlgebra.IsKilling.chainLength α β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<GOAL>LieAlgebra.IsKilling.chainLength (-α) β = LieAlgebra.IsKilling.chainLength α β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>β : LieModule.Weight K (↥H) L<VAR>Nontrivial L<GOAL>LieAlgebra.IsKilling.chainLength 0 β = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<GOAL>β (LieAlgebra.IsKilling.coroot α) = ↑(↑(LieModule.chainBotCoeff (⇑α) β) - ↑(LieModule.chainTopCoeff (⇑α) β))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℤ<VAR>hn : LieAlgebra.rootSpace H (-n • ⇑α + ⇑β) ≠ ⊥<GOAL>n ≤ ↑(LieModule.chainBotCoeff (⇑α) β)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℤ<GOAL>LieAlgebra.rootSpace H (n • ⇑α + ⇑β) ≠ ⊥ ↔ n ≤ ↑(LieModule.chainTopCoeff (⇑α) β) ∧ -n ≤ ↑(LieModule.chainBotCoeff (⇑α) β)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℤ<GOAL>LieAlgebra.rootSpace H (n • ⇑α + ⇑β) ≠ ⊥ ↔ n ∈ Finset.Icc (-↑(LieModule.chainBotCoeff (⇑α) β)) ↑(LieModule.chainTopCoeff (⇑α) β)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>β' : LieModule.Weight K (↥H) L<VAR>n : ℤ<VAR>hβ' : ⇑β' = n • ⇑α + ⇑β<GOAL>↑(LieModule.chainTopCoeff (⇑α) β') = ↑(LieModule.chainTopCoeff (⇑α) β) - n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>β' : LieModule.Weight K (↥H) L<VAR>n : ℤ<VAR>hβ' : ⇑β' = n • ⇑α + ⇑β<GOAL>↑(LieModule.chainBotCoeff (⇑α) β') = ↑(LieModule.chainBotCoeff (⇑α) β) + n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β β' : LieModule.Weight K (↥H) L<VAR>n : ℤ<VAR>hβ' : ⇑β' = n • ⇑α + ⇑β<GOAL>LieAlgebra.IsKilling.chainLength α β' = LieAlgebra.IsKilling.chainLength α β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>Nontrivial L<GOAL>LieModule.chainTopCoeff (⇑α) 0 = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>Nontrivial L<GOAL>LieModule.chainBotCoeff (⇑α) 0 = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>Nontrivial L<GOAL>LieAlgebra.IsKilling.chainLength α 0 = 2
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>LieAlgebra.rootSpace H (2 • ⇑α) = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>LieAlgebra.rootSpace H (2⁻¹ • ⇑α) = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<GOAL>k = -1 ∨ k = 0 ∨ k = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hβ : β.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<GOAL>β = -α ∨ β = α
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : LieModule.Weight K (↥H) L<VAR>hβ : β.IsNonZero<GOAL>(LieAlgebra.IsKilling.reflectRoot α β).IsNonZero
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>f : Module.Dual K ↥H<VAR>x : ↥H<GOAL>((LieAlgebra.IsKilling.rootSystem H).toLin f) x = f x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : { α // α.IsNonZero }<GOAL>(LieAlgebra.IsKilling.rootSystem H).pairing β α = ↑β (LieAlgebra.IsKilling.coroot ↑α)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : { α // α.IsNonZero }<GOAL>(LieAlgebra.IsKilling.rootSystem H).root α = LieModule.Weight.toLinear K (↥H) L ↑α
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : { α // α.IsNonZero }<GOAL>(LieAlgebra.IsKilling.rootSystem H).coroot α = LieAlgebra.IsKilling.coroot ↑α