ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g<VAR>ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b<GOAL>(CategoryTheory.Bicategory.rightZigzagIso η ε).symm = CategoryTheory.Bicategory.leftZigzagIso ε.symm η.symm
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g<VAR>ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b<VAR>h : CategoryTheory.Bicategory.leftZigzag η.hom ε.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.Bicategory.rightUnitor f).inv<GOAL>CategoryTheory.Bicategory.rightZigzag η.hom ε.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom (CategoryTheory.Bicategory.leftUnitor g).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g<VAR>ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b<GOAL>CategoryTheory.Bicategory.leftZigzagIso η (CategoryTheory.Bicategory.adjointifyCounit η ε) = CategoryTheory.Bicategory.leftUnitor f ≪≫ (CategoryTheory.Bicategory.rightUnitor f).symm
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>self : CategoryTheory.Bicategory.Equivalence a b<GOAL>CategoryTheory.Bicategory.leftZigzagIso self.unit self.counit = CategoryTheory.Bicategory.leftUnitor self.hom ≪≫ (CategoryTheory.Bicategory.rightUnitor self.hom).symm
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>e : CategoryTheory.Bicategory.Equivalence a b<GOAL>CategoryTheory.Bicategory.leftZigzag e.unit.hom e.counit.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor e.hom).hom (CategoryTheory.Bicategory.rightUnitor e.hom).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>e : CategoryTheory.Bicategory.Equivalence a b<GOAL>CategoryTheory.Bicategory.rightZigzagIso e.unit e.counit = CategoryTheory.Bicategory.rightUnitor e.inv ≪≫ (CategoryTheory.Bicategory.leftUnitor e.inv).symm
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>e : CategoryTheory.Bicategory.Equivalence a b<GOAL>CategoryTheory.Bicategory.rightZigzag e.unit.hom e.counit.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor e.inv).hom (CategoryTheory.Bicategory.leftUnitor e.inv).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>left : a ⟶ b<VAR>self : CategoryTheory.Bicategory.IsLeftAdjoint left<GOAL>Nonempty (CategoryTheory.Bicategory.RightAdjoint left)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>adj : CategoryTheory.Bicategory.Adjunction f g<GOAL>CategoryTheory.Bicategory.IsLeftAdjoint f
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>right : b ⟶ a<VAR>self : CategoryTheory.Bicategory.IsRightAdjoint right<GOAL>Nonempty (CategoryTheory.Bicategory.LeftAdjoint right)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>adj : CategoryTheory.Bicategory.Adjunction f g<GOAL>CategoryTheory.Bicategory.IsRightAdjoint g
<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>LieModule.IsIrreducible R L M<GOAL>Nontrivial M
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.HasTrivialRadical R L<VAR>I : LieIdeal R L<VAR>hI : LieAlgebra.IsSolvable R ↥↑I<GOAL>I = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.HasTrivialRadical R L<GOAL>LieAlgebra.center R L = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>h : ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable R ↥↑I → I = ⊥<GOAL>LieAlgebra.HasTrivialRadical R L
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>LieAlgebra.HasTrivialRadical R L ↔ ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable R ↥↑I → I = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>LieAlgebra.HasTrivialRadical R L ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥↑I → I = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsSimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<GOAL>I = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsSimple R L<GOAL>IsAtom ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsSimple R L<VAR>I : LieIdeal R L<GOAL>IsAtom I ↔ I = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsSemisimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<GOAL>LieAlgebra.IsSimple R ↥↑I
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsSemisimple R L<VAR>s : Finset (LieIdeal R L)<GOAL>↑s ⊆ {I | IsAtom I} → ∀ I ≤ s.sup id, ∃ t ⊆ s, I = t.sup id
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsSemisimple R L<GOAL>IsCompactlyGenerated.BooleanGenerators {I | IsAtom I}
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.HasTrivialRadical R L<VAR>h : IsLieAbelian L<GOAL>Subsingleton L
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.HasTrivialRadical R L<GOAL>IsLieAbelian ↥↑(LieAlgebra.radical R L)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>IsNoetherian R L<GOAL>IsLieAbelian ↥↑(LieAlgebra.radical R L) ↔ ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable R ↥↑I → IsLieAbelian ↥↑I
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.HasTrivialRadical R L<GOAL>(LieAlgebra.ad R L).ker = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>Field R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<GOAL>(killingForm R (LieDerivation R L L)).restrict (LieDerivation.ad R L).range.toSubmodule = killingForm R ↥(LieDerivation.ad R L).range
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>Field R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>↑(LieDerivation.IsKilling.rangeAdOrthogonal R L) = {m | ∀ (a : L), (killingForm R (LieDerivation R L L)).IsOrtho ((LieDerivation.ad R L) a) m}
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>Field R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>D : LieDerivation R L L<VAR>hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (LieDerivation.ad R L).range.toSubmodule<VAR>x : L<GOAL>(LieDerivation.ad R L) (D x) ∈ (killingForm R (LieDerivation R L L)).orthogonal (LieDerivation.ad R L).range.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>Field R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>D : LieDerivation R L L<VAR>hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (LieDerivation.ad R L).range.toSubmodule<VAR>x : L<GOAL>(LieDerivation.ad R L) (D x) ∈ Submodule.map (LieDerivation.ad R L).range.subtype (LinearMap.ker (killingForm R ↥(LieDerivation.ad R L).range))
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>Field R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>LieAlgebra.IsKilling R L<VAR>x : L<GOAL>(LieDerivation.ad R L) x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>Field R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>LieAlgebra.IsKilling R L<GOAL>((killingForm R (LieDerivation R L L)).restrict (LieDerivation.ad R L).range.toSubmodule).Nondegenerate
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>Field R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>LieAlgebra.IsKilling R L<GOAL>(LieDerivation.ad R L).range = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>Field R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Module.Finite R L<VAR>LieAlgebra.IsKilling R L<VAR>D : LieDerivation R L L<GOAL>∃ x, (LieDerivation.ad R L) x = D
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>y : L<GOAL>∃ t, ∃ z ∈ I, y = t • x + z
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>M : Type u₄<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<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>N : LieSubmodule R L M<GOAL>↑⁅⊤, N⁆ = Submodule.map ((LieModule.toEnd R L M) x) ↑N ⊔ ↑⁅I, N⁆
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>M : Type u₄<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<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>n i j : ℕ<VAR>hxn : (LieModule.toEnd R L M) x ^ n = 0<VAR>hIM : LieModule.lowerCentralSeries R L M i ≤ I.lcs M j<GOAL>LieModule.lowerCentralSeries R L M (i + n) ≤ I.lcs M (j + 1)
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>M : Type u₄<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<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>hnp : IsNilpotent ((LieModule.toEnd R L M) x)<VAR>hIM : LieModule.IsNilpotent R (↥↑I) M<GOAL>LieModule.IsNilpotent R L M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Subsingleton L<GOAL>LieAlgebra.IsEngelian R L
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>hf : Function.Surjective ⇑f<VAR>h : LieAlgebra.IsEngelian R L<GOAL>LieAlgebra.IsEngelian R L₂
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>e : L ≃ₗ⁅R⁆ L₂<GOAL>LieAlgebra.IsEngelian R L ↔ LieAlgebra.IsEngelian R L₂
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K : LieSubalgebra R L<VAR>hK₁ : LieAlgebra.IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<GOAL>∃ K', LieAlgebra.IsEngelian R ↥K' ∧ K < K'
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>IsNoetherian R L<GOAL>LieAlgebra.IsEngelian R L
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>M : Type u₄<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>IsNoetherian R L<GOAL>LieModule.IsNilpotent R L M ↔ ∀ (x : L), IsNilpotent ((LieModule.toEnd R L M) x)
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>M : Type u₄<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>IsNoetherian R M<GOAL>LieModule.IsNilpotent R L M ↔ ∀ (x : L), IsNilpotent ((LieModule.toEnd R L M) x)
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>IsNoetherian R L<GOAL>LieAlgebra.IsNilpotent R L ↔ ∀ (x : L), IsNilpotent ((LieAlgebra.ad R L) x)
<VAR>ι : Type v<VAR>L : Type w₁<VAR>M : ι → Type w<VAR>LieRing L<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → LieRingModule L (M i)<VAR>x : L<VAR>m : DirectSum ι fun i => M i<VAR>i : ι<GOAL>⁅x, m⁆ i = ⁅x, m i⁆
<VAR>ι : Type v<VAR>L : ι → Type w<VAR>(i : ι) → LieRing (L i)<VAR>x y : DirectSum ι fun i => L i<VAR>i : ι<GOAL>⁅x, y⁆ i = ⁅x i, y i⁆
<VAR>ι : Type v<VAR>L : ι → Type w<VAR>(i : ι) → LieRing (L i)<VAR>DecidableEq ι<VAR>i : ι<VAR>x y : L i<GOAL>⁅(DirectSum.of L i) x, (DirectSum.of L i) y⁆ = (DirectSum.of L i) ⁅x, y⁆
<VAR>ι : Type v<VAR>L : ι → Type w<VAR>(i : ι) → LieRing (L i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : L i<VAR>y : L j<GOAL>⁅(DirectSum.of L i) x, (DirectSum.of L j) y⁆ = 0
<VAR>ι : Type v<VAR>L : ι → Type w<VAR>(i : ι) → LieRing (L i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>x : L i<VAR>y : L j<GOAL>⁅(DirectSum.of L i) x, (DirectSum.of L j) y⁆ = if hij : i = j then (DirectSum.of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0
<VAR>R : Type u<VAR>ι : Type v<VAR>CommRing R<VAR>L : ι → Type w<VAR>(i : ι) → LieRing (L i)<VAR>(i : ι) → LieAlgebra R (L i)<VAR>DecidableEq ι<VAR>j : ι<VAR>a : L j<GOAL>(DirectSum.lieAlgebraOf R ι L j) a = (DirectSum.of L j) a
<VAR>R : Type u<VAR>ι : Type v<VAR>CommRing R<VAR>L : ι → Type w<VAR>(i : ι) → LieRing (L i)<VAR>(i : ι) → LieAlgebra R (L i)<VAR>j : ι<VAR>a : DirectSum ι fun i => L i<GOAL>(DirectSum.lieAlgebraComponent R ι L j) a = (DirectSum.component R ι L j) a
<VAR>R : Type u<VAR>ι : Type v<VAR>CommRing R<VAR>L : ι → Type w<VAR>(i : ι) → LieRing (L i)<VAR>(i : ι) → LieAlgebra R (L i)<VAR>x y : DirectSum ι fun i => L i<VAR>h : ∀ (i : ι), (DirectSum.lieAlgebraComponent R ι L i) x = (DirectSum.lieAlgebraComponent R ι L i) y<GOAL>x = y
<VAR>R : Type u<VAR>ι : Type v<VAR>CommRing R<VAR>L : ι → Type w<VAR>(i : ι) → LieRing (L i)<VAR>(i : ι) → LieAlgebra R (L i)<VAR>DecidableEq ι<VAR>L' : Type w₁<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : (i : ι) → L i →ₗ⁅R⁆ L'<VAR>hf : Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0<VAR>a : DirectSum ι fun i => L i<GOAL>(DirectSum.toLieAlgebra L' f hf) a = (DirectSum.toModule R ι L' fun i => ↑(f i)) a
<VAR>A : Type v<VAR>Ring A<VAR>x y : A<GOAL>⁅x, y⁆ = x * y - y * x
<VAR>A : Type v<VAR>Ring A<VAR>α : Type u_1<VAR>f g : α → A<VAR>a : α<GOAL>⁅f, g⁆ a = ⁅f a, g a⁆
<VAR>A : Type v<VAR>Ring A<VAR>M : Type w<VAR>AddCommGroup M<VAR>Module A M<VAR>a : A<VAR>m : M<GOAL>⁅a, m⁆ = a • m
<VAR>A : Type v<VAR>Ring A<VAR>R : Type u<VAR>CommRing R<VAR>Algebra R A<VAR>M : Type w<VAR>AddCommGroup M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<GOAL>LieModule R A M
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type w<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>m : M<GOAL>⁅f, m⁆ = f m
<VAR>A : Type v<VAR>Ring A<VAR>R : Type u<VAR>CommRing R<VAR>Algebra R A<VAR>B : Type w<VAR>Ring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>⇑f.toLieHom = ⇑f
<VAR>A : Type v<VAR>Ring A<VAR>R : Type u<VAR>CommRing R<VAR>Algebra R A<VAR>B : Type w<VAR>Ring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>x : A<GOAL>f.toLieHom x = f x
<VAR>A : Type v<VAR>Ring A<VAR>R : Type u<VAR>CommRing R<VAR>Algebra R A<GOAL>(AlgHom.id R A).toLieHom = LieHom.id
<VAR>A : Type v<VAR>Ring A<VAR>R : Type u<VAR>CommRing R<VAR>Algebra R A<VAR>B : Type w<VAR>C : Type w₁<VAR>Ring B<VAR>Ring C<VAR>Algebra R B<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : B →ₐ[R] C<GOAL>(g.comp f).toLieHom = g.toLieHom.comp f.toLieHom
<VAR>A : Type v<VAR>Ring A<VAR>R : Type u<VAR>CommRing R<VAR>Algebra R A<VAR>B : Type w<VAR>Ring B<VAR>Algebra R B<VAR>f g : A →ₐ[R] B<VAR>h : f.toLieHom = g.toLieHom<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>x : L<VAR>m : M<GOAL>((LieModule.toEnd R L M) x) m = ⁅x, m⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x y : L<GOAL>((LieAlgebra.ad R L) x) y = ⁅x, y⁆
<VAR>R : Type u<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>LieModule.toEnd R (Module.End R M) M = LieHom.id
<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>K : LieSubalgebra R L<VAR>x : ↥K<GOAL>(LieModule.toEnd R (↥K) M) x = (LieModule.toEnd R L M) ↑x
<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>K : LieSubalgebra R L<VAR>x : L<VAR>hx : x ∈ K<GOAL>(LieModule.toEnd R (↥K) M) ⟨x, hx⟩ = (LieModule.toEnd R L M) x
<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<VAR>y : ↥N<GOAL>↑(((LieModule.toEnd R L ↥↑N) x) y) = ((LieModule.toEnd R L M) x) ↑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<VAR>x : L<VAR>y : ↥N<VAR>n : ℕ<GOAL>↑(((LieModule.toEnd R L ↥↑N) x ^ n) y) = ((LieModule.toEnd R L M) x ^ n) ↑y
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>x y : ↥H<GOAL>↑(((LieAlgebra.ad R ↥H) x) y) = ((LieAlgebra.ad R L) ↑x) ↑y
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>x y : ↥H<VAR>n : ℕ<GOAL>↑(((LieAlgebra.ad R ↥H) x ^ n) y) = ((LieAlgebra.ad R L) ↑x ^ n) ↑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>x y : L<VAR>z : M<GOAL>((LieModule.toEnd R L M) x) ⁅y, z⁆ = ⁅((LieAlgebra.ad R L) x) y, z⁆ + ⁅y, ((LieModule.toEnd R L M) x) z⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x y z : L<GOAL>((LieAlgebra.ad R L) x) ⁅y, z⁆ = ⁅((LieAlgebra.ad R L) x) y, z⁆ + ⁅y, ((LieAlgebra.ad R L) x) z⁆
<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 y : L<VAR>z : M<VAR>n : ℕ<GOAL>((LieModule.toEnd R L M) x ^ n) ⁅y, z⁆ = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((LieModule.toEnd R L M) x ^ ij.2) z⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x y z : L<VAR>n : ℕ<GOAL>((LieAlgebra.ad R L) x ^ n) ⁅y, z⁆ = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((LieAlgebra.ad R L) x ^ ij.2) z⁆
<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₂ : Type w₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>k : ℕ<VAR>x : L<GOAL>((LieModule.toEnd R L M₂) x ^ k) ∘ₗ ↑f = ↑f ∘ₗ (LieModule.toEnd R L M) x ^ k
<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₂ : Type w₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>k : ℕ<VAR>x : L<VAR>m : M<GOAL>((LieModule.toEnd R L M₂) x ^ k) (f m) = f (((LieModule.toEnd R L M) x ^ k) m)
<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>Submodule.map ((LieModule.toEnd R L M) x) ↑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>x : L<VAR>m : M<VAR>hm : m ∈ ↑N<GOAL>((LieModule.toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑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>x : L<VAR>h : ∀ (m : M) (hm : m ∈ ↑N), ((LieModule.toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N := ⋯<GOAL>LinearMap.restrict ((LieModule.toEnd R L M) x) h = (LieModule.toEnd R L ↥↑N) x
<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>φ : R<VAR>k : ℕ<VAR>x : L<GOAL>Set.MapsTo ⇑(((LieModule.toEnd R L M) x - (algebraMap R (Module.End R M)) φ) ^ k) ↑N ↑N
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type v<VAR>Ring A<VAR>Algebra R A<GOAL>⇑(LieAlgebra.ad R A) = LinearMap.mulLeft R - LinearMap.mulRight R
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K : LieSubalgebra R L<VAR>x : ↥K<GOAL>(LieAlgebra.ad R L) ↑x ∘ₗ ↑K.incl = ↑K.incl ∘ₗ (LieAlgebra.ad R ↥K) x
<VAR>R : Type u<VAR>M₁ : Type v<VAR>M₂ : Type w<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>e : M₁ ≃ₗ[R] M₂<VAR>f : Module.End R M₁<GOAL>e.lieConj f = e.conj f
<VAR>R : Type u<VAR>M₁ : Type v<VAR>M₂ : Type w<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>e : M₁ ≃ₗ[R] M₂<GOAL>e.lieConj.symm = e.symm.lieConj
<VAR>R : Type u<VAR>A₁ : Type v<VAR>A₂ : Type w<VAR>CommRing R<VAR>Ring A₁<VAR>Ring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>x : A₁<GOAL>e.toLieEquiv x = e x
<VAR>R : Type u<VAR>A₁ : Type v<VAR>A₂ : Type w<VAR>CommRing R<VAR>Ring A₁<VAR>Ring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>x : A₂<GOAL>e.toLieEquiv.symm x = e.symm 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>e : L ≃ₗ⁅R⁆ L'<VAR>x : L<GOAL>e.toLinearEquiv.conj ((LieAlgebra.ad R L) x) = (LieAlgebra.ad R L') (e x)
<VAR>R : Type u_2<VAR>Add R<VAR>c : R<VAR>self : IsAddRegular c<GOAL>IsAddLeftRegular c
<VAR>R : Type u_2<VAR>Add R<VAR>c : R<VAR>self : IsAddRegular c<GOAL>IsAddRightRegular c
<VAR>R : Type u_1<VAR>Mul R<VAR>c : R<VAR>self : IsRegular c<GOAL>IsLeftRegular c
<VAR>R : Type u_1<VAR>Mul R<VAR>c : R<VAR>self : IsRegular c<GOAL>IsRightRegular c
<VAR>R : Type u_1<VAR>Mul R<VAR>c : R<GOAL>IsRegular c ↔ IsLeftRegular c ∧ IsRightRegular c
<VAR>R : Type u_1<VAR>Add R<VAR>c : R<GOAL>IsAddRegular c ↔ IsAddLeftRegular c ∧ IsAddRightRegular c
<VAR>R : Type u_1<VAR>Add R<VAR>PartialOrder R<VAR>a : R<VAR>ha : AddLECancellable a<GOAL>IsAddLeftRegular a
<VAR>R : Type u_1<VAR>Mul R<VAR>PartialOrder R<VAR>a : R<VAR>ha : MulLECancellable a<GOAL>IsLeftRegular a
<VAR>R : Type u_1<VAR>Mul R<VAR>a : R<VAR>ca : ∀ (b : R), Commute a b<VAR>h : IsLeftRegular a<GOAL>IsRightRegular a
<VAR>R : Type u_1<VAR>Mul R<VAR>a : R<VAR>ca : ∀ (b : R), Commute a b<VAR>h : IsRightRegular a<GOAL>IsLeftRegular a
<VAR>R : Type u_1<VAR>Mul R<VAR>a : R<VAR>ca : ∀ (b : R), Commute a b<GOAL>IsRightRegular a ↔ IsLeftRegular a
<VAR>R : Type u_1<VAR>Mul R<VAR>a : R<VAR>ca : ∀ (b : R), Commute a b<GOAL>IsRegular a ↔ IsLeftRegular a
<VAR>R : Type u_1<VAR>AddSemigroup R<VAR>a b : R<VAR>lra : IsAddLeftRegular a<VAR>lrb : IsAddLeftRegular b<GOAL>IsAddLeftRegular (a + b)
<VAR>R : Type u_1<VAR>Semigroup R<VAR>a b : R<VAR>lra : IsLeftRegular a<VAR>lrb : IsLeftRegular b<GOAL>IsLeftRegular (a * b)
<VAR>R : Type u_1<VAR>Semigroup R<VAR>a b : R<VAR>rra : IsRightRegular a<VAR>rrb : IsRightRegular b<GOAL>IsRightRegular (a * b)
<VAR>R : Type u_1<VAR>AddSemigroup R<VAR>a b : R<VAR>rra : IsAddRightRegular a<VAR>rrb : IsAddRightRegular b<GOAL>IsAddRightRegular (a + b)
<VAR>R : Type u_1<VAR>Semigroup R<VAR>a b : R<VAR>rra : IsRegular a<VAR>rrb : IsRegular b<GOAL>IsRegular (a * b)
<VAR>R : Type u_1<VAR>AddSemigroup R<VAR>a b : R<VAR>rra : IsAddRegular a<VAR>rrb : IsAddRegular b<GOAL>IsAddRegular (a + b)
<VAR>R : Type u_1<VAR>AddSemigroup R<VAR>a b : R<VAR>ab : IsAddLeftRegular (a + b)<GOAL>IsAddLeftRegular b
<VAR>R : Type u_1<VAR>Semigroup R<VAR>a b : R<VAR>ab : IsLeftRegular (a * b)<GOAL>IsLeftRegular b
<VAR>R : Type u_1<VAR>Semigroup R<VAR>a : R<VAR>b : R<VAR>ha : IsLeftRegular a<GOAL>IsLeftRegular (a * b) ↔ IsLeftRegular b
<VAR>R : Type u_1<VAR>AddSemigroup R<VAR>a : R<VAR>b : R<VAR>ha : IsAddLeftRegular a<GOAL>IsAddLeftRegular (a + b) ↔ IsAddLeftRegular b
<VAR>R : Type u_1<VAR>AddSemigroup R<VAR>a b : R<VAR>ab : IsAddRightRegular (b + a)<GOAL>IsAddRightRegular b
<VAR>R : Type u_1<VAR>Semigroup R<VAR>a b : R<VAR>ab : IsRightRegular (b * a)<GOAL>IsRightRegular b
<VAR>R : Type u_1<VAR>AddSemigroup R<VAR>a : R<VAR>b : R<VAR>ha : IsAddRightRegular a<GOAL>IsAddRightRegular (b + a) ↔ IsAddRightRegular b
<VAR>R : Type u_1<VAR>Semigroup R<VAR>a : R<VAR>b : R<VAR>ha : IsRightRegular a<GOAL>IsRightRegular (b * a) ↔ IsRightRegular b