ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddBelow s<GOAL>sSup s⁻¹ = (sInf s)⁻¹
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<GOAL>sInf (-s) = -sSup s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<GOAL>sInf s⁻¹ = (sSup s)⁻¹
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddAbove t<GOAL>sSup (s * t) = sSup s * sSup t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddAbove t<GOAL>sSup (s + t) = sSup s + sSup t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddBelow s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddBelow t<GOAL>sInf (s + t) = sInf s + sInf t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddBelow s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddBelow t<GOAL>sInf (s * t) = sInf s * sInf t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddBelow t<GOAL>sSup (s / t) = sSup s / sInf t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddBelow t<GOAL>sSup (s - t) = sSup s - sInf t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddBelow s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddAbove t<GOAL>sInf (s / t) = sInf s / sSup t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddBelow s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddAbove t<GOAL>sInf (s - t) = sInf s - sSup t
<VAR>K : Type u_2<VAR>LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<GOAL>r • Set.Ioo a b = Set.Ioo (r • a) (r • b)
<VAR>K : Type u_2<VAR>LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<GOAL>r • Set.Icc a b = Set.Icc (r • a) (r • b)
<VAR>K : Type u_2<VAR>LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<GOAL>r • Set.Ico a b = Set.Ico (r • a) (r • b)
<VAR>K : Type u_2<VAR>LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<GOAL>r • Set.Ioc a b = Set.Ioc (r • a) (r • b)
<VAR>K : Type u_2<VAR>LinearOrderedField K<VAR>a r : K<VAR>hr : 0 < r<GOAL>r • Set.Ioi a = Set.Ioi (r • a)
<VAR>K : Type u_2<VAR>LinearOrderedField K<VAR>a r : K<VAR>hr : 0 < r<GOAL>r • Set.Iio a = Set.Iio (r • a)
<VAR>K : Type u_2<VAR>LinearOrderedField K<VAR>a r : K<VAR>hr : 0 < r<GOAL>r • Set.Ici a = Set.Ici (r • a)
<VAR>K : Type u_2<VAR>LinearOrderedField K<VAR>a r : K<VAR>hr : 0 < r<GOAL>r • Set.Iic a = Set.Iic (r • a)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>χ : LieAlgebra.LieCharacter R L<VAR>x y : L<GOAL>χ ⁅x, y⁆ = 0
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>χ : LieAlgebra.LieCharacter R L<VAR>x y : L<GOAL>⁅χ x, χ y⁆ = 0
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>χ : LieAlgebra.LieCharacter R L<VAR>x : L<VAR>h : x ∈ LieAlgebra.derivedSeries R L 1<GOAL>χ x = 0
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>IsLieAbelian L<VAR>χ : LieAlgebra.LieCharacter R L<GOAL>LieAlgebra.lieCharacterEquivLinearDual χ = ↑χ
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>IsLieAbelian L<VAR>ψ : Module.Dual R L<GOAL>LieAlgebra.lieCharacterEquivLinearDual.symm ψ = { toLinearMap := ψ, map_lie' := ⋯ }
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>Φ : LinearMap.BilinForm R M<VAR>LieModule R L M<GOAL>LinearMap.BilinForm.lieInvariant L Φ ↔ Φ ∈ LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>Φ : LinearMap.BilinForm R M<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>N : LieSubmodule R L M<GOAL>↑(LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N) = {m | ∀ n ∈ N, Φ.IsOrtho n m}
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>Φ : LinearMap.BilinForm R M<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>N : LieSubmodule R L M<GOAL>↑(LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N) = Φ.orthogonal ↑N
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>Φ : LinearMap.BilinForm R M<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>N : LieSubmodule R L M<VAR>y : M<GOAL>y ∈ LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N ↔ ∀ x ∈ N, (Φ x) y = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<GOAL>Disjoint I (LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : IsAtom I<GOAL>IsCompl ↑I ↑(LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : IsAtom I<GOAL>IsCompl I (LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : IsAtom I<GOAL>(Φ.restrict (lieIdealSubalgebra K L I).toSubmodule).Nondegenerate
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : IsAtom I<GOAL>(Φ.restrict (lieIdealSubalgebra K L (LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)).toSubmodule).Nondegenerate
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<GOAL>sSup {J | IsAtom J ∧ J ≤ I} = I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<GOAL>LieAlgebra.IsSemisimple K L
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>self : LieAlgebra.IsKilling R L<GOAL>LieIdeal.killingCompl R L ⊤ = ⊥
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsKilling R L<GOAL>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>LieAlgebra.IsKilling R L<GOAL>(killingForm R L).Nondegenerate
<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>LieAlgebra.IsKilling R L<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>I : LieIdeal R L<VAR>IsLieAbelian ↥↑I<GOAL>I = ⊥
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : Type u_5<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>e : L ≃ₗ⁅R⁆ L'<VAR>x y : L<GOAL>((killingForm R L') (e x)) (e y) = ((killingForm R L) x) y
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : Type u_5<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>LieAlgebra.IsKilling R L<VAR>e : L ≃ₗ⁅R⁆ L'<GOAL>LieAlgebra.IsKilling R L'
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>ι : Type u_5<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R L<GOAL>((↑(LieModule.toEnd R L M)).polyCharpoly b).coeff (LieModule.rank R L M) ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>ι : Type u_5<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R L<GOAL>LieModule.rank R L M = ((↑(LieModule.toEnd R L M)).polyCharpoly b).natTrailingDegree
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>ιₘ : Type u_6<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>Fintype ιₘ<VAR>bₘ : Basis ιₘ R M<GOAL>LieModule.rank R L M ≤ Fintype.card ιₘ
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R M<VAR>Module.Free R M<GOAL>LieModule.rank R L M ≤ FiniteDimensional.finrank R M
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>x : L<GOAL>LieModule.rank R L M ≤ (LinearMap.charpoly ((LieModule.toEnd R L M) x)).natTrailingDegree
<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>Module.Finite R L<VAR>Module.Free R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>x : L<GOAL>LieModule.IsRegular R M x ↔ (LinearMap.charpoly ((LieModule.toEnd R L M) x)).coeff (LieModule.rank R L M) ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>ι : Type u_5<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R L<VAR>x : L<GOAL>LieModule.IsRegular R M x ↔ (MvPolynomial.eval ⇑(b.repr x)) (((↑(LieModule.toEnd R L M)).polyCharpoly b).coeff (LieModule.rank R L M)) ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>x : L<GOAL>LieModule.IsRegular R M x ↔ (LinearMap.charpoly ((LieModule.toEnd R L M) x)).natTrailingDegree = LieModule.rank R L M
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>IsDomain R<VAR>h : ↑(FiniteDimensional.finrank R M) ≤ Cardinal.mk R<GOAL>∃ x, LieModule.IsRegular R M x
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>IsDomain R<VAR>Infinite R<GOAL>∃ x, LieModule.IsRegular R M x
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R L<GOAL>((↑(LieAlgebra.ad R L)).polyCharpoly b).coeff (LieAlgebra.rank R L) ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R L<GOAL>LieAlgebra.rank R L = ((↑(LieAlgebra.ad R L)).polyCharpoly b).natTrailingDegree
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Fintype ι<VAR>b : Basis ι R L<GOAL>LieAlgebra.rank R L ≤ Fintype.card ι
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<GOAL>LieAlgebra.rank R L ≤ FiniteDimensional.finrank R L
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>x : L<GOAL>LieAlgebra.rank R L ≤ (LinearMap.charpoly ((LieAlgebra.ad R L) x)).natTrailingDegree
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>x : L<GOAL>LieAlgebra.IsRegular R x ↔ (LinearMap.charpoly ((LieAlgebra.ad R L) x)).coeff (LieAlgebra.rank R L) ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R L<VAR>x : L<GOAL>LieAlgebra.IsRegular R x ↔ (MvPolynomial.eval ⇑(b.repr x)) (((↑(LieAlgebra.ad R L)).polyCharpoly b).coeff (LieAlgebra.rank R L)) ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>x : L<GOAL>LieAlgebra.IsRegular R x ↔ (LinearMap.charpoly ((LieAlgebra.ad R L) x)).natTrailingDegree = LieAlgebra.rank R L
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>IsDomain R<VAR>h : ↑(FiniteDimensional.finrank R L) ≤ Cardinal.mk R<GOAL>∃ x, LieAlgebra.IsRegular R x
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>IsDomain R<VAR>Infinite R<GOAL>∃ x, LieAlgebra.IsRegular R x
<VAR>K : Type u_7<VAR>L : Type u_8<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>x : L<GOAL>FiniteDimensional.finrank K ↥(LieSubalgebra.engel K x) = (LinearMap.charpoly ((LieAlgebra.ad K L) x)).natTrailingDegree
<VAR>K : Type u_7<VAR>L : Type u_8<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>x : L<GOAL>LieAlgebra.rank K L ≤ FiniteDimensional.finrank K ↥(LieSubalgebra.engel K x)
<VAR>K : Type u_7<VAR>L : Type u_8<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>x : L<GOAL>LieAlgebra.IsRegular K x ↔ FiniteDimensional.finrank K ↥(LieSubalgebra.engel K x) = LieAlgebra.rank K L
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : L<GOAL>↑(LieSubalgebra.engel R x) = ⋂ s ∈ fun x_1 => ∀ (a : ℕ), LinearMap.ker ((LieAlgebra.ad R L) x ^ a) ≤ x_1, ↑s
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x y : L<GOAL>y ∈ LieSubalgebra.engel R x ↔ ∃ n, ((LieAlgebra.ad R L) x ^ n) y = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : L<GOAL>x ∈ LieSubalgebra.engel R x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>LieSubalgebra.engel R 0 = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : L<GOAL>(LieSubalgebra.engel R x).normalizer = LieSubalgebra.engel R x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>h : LieSubalgebra.engel R x ≤ H<GOAL>H.normalizer = H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>h : ∀ x ∈ H, H ≤ LieSubalgebra.engel R x<GOAL>LieAlgebra.IsNilpotent R ↥H
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>a : L<GOAL>f.toNonUnitalAlgHom a = f a
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<GOAL>Function.Injective LieHom.toNonUnitalAlgHom
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<VAR>m : M<GOAL>Quotient.mk'' m = LieSubmodule.Quotient.mk m
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>x y : L<GOAL>LieSubmodule.Quotient.mk ⁅x, y⁆ = ⁅LieSubmodule.Quotient.mk x, LieSubmodule.Quotient.mk y⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<GOAL>∀ (a : M), (LieSubmodule.Quotient.mk' N) a = LieSubmodule.Quotient.mk a
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<GOAL>Function.Surjective ⇑(LieSubmodule.Quotient.mk' N)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<GOAL>(LieSubmodule.Quotient.mk' N).range = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<VAR>m : M<GOAL>(LieSubmodule.Quotient.mk' N) m = 0 ↔ m ∈ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<VAR>m : M<GOAL>LieSubmodule.Quotient.mk m = 0 ↔ m ∈ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<GOAL>(LieSubmodule.Quotient.mk' N).ker = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N N' : LieSubmodule R L M<GOAL>LieSubmodule.map (LieSubmodule.Quotient.mk' N) N' = ⊥ ↔ N' ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<VAR>f g : M ⧸ N →ₗ⁅R,L⁆ M<VAR>h : f.comp (LieSubmodule.Quotient.mk' N) = g.comp (LieSubmodule.Quotient.mk' N)<GOAL>f = g
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<VAR>x : L<GOAL>(LieModule.toEnd R L (M ⧸ N)) x ∘ₗ ↑(LieSubmodule.Quotient.mk' N) = ↑(LieSubmodule.Quotient.mk' N) ∘ₗ (LieModule.toEnd R L M) x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>a : L ⧸ LinearMap.ker ↑f<GOAL>f.quotKerEquivRange a = (↑f).quotKerEquivRange a
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>∀ (a : ↥(LinearMap.range ↑f)), f.quotKerEquivRange.invFun a = (↑f).quotKerEquivRange.invFun a
<VAR>L : Type v<VAR>M : Type w<VAR>Bracket L M<VAR>Zero M<VAR>self : LieModule.IsTrivial L M<VAR>x : L<VAR>m : M<GOAL>⁅x, m⁆ = 0
<VAR>L : Type v<VAR>M : Type w<VAR>Bracket L M<VAR>Zero M<VAR>LieModule.IsTrivial L M<VAR>x : L<VAR>m : M<GOAL>⁅x, m⁆ = 0
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₁<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>h₁ : Function.Injective ⇑f<GOAL>IsLieAbelian L₂ → IsLieAbelian L₁
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₁<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>h₁ : Function.Surjective ⇑f<VAR>h₂ : IsLieAbelian L₁<GOAL>IsLieAbelian L₂
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₁<VAR>LieAlgebra R L₂<VAR>e : L₁ ≃ₗ⁅R⁆ L₂<GOAL>IsLieAbelian L₁ ↔ IsLieAbelian L₂
<VAR>A : Type v<VAR>Ring A<GOAL>(Std.Commutative fun x x_1 => x * x_1) ↔ IsLieAbelian A
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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.ker R L M ↔ ∀ (m : M), ⁅x, m⁆ = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>m : M<GOAL>m ∈ LieModule.maxTrivSubmodule R L M ↔ ∀ (x : L), ⁅x, m⁆ = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>I : LieIdeal R L<GOAL>⁅I, LieModule.maxTrivSubmodule R L M⁆ = ⊥