ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>N ≤ LieModule.maxTrivSubmodule R L 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>LieModule.IsTrivial L ↥↑N ↔ N ≤ LieModule.maxTrivSubmodule R L 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<GOAL>LieModule.IsTrivial L M ↔ LieModule.maxTrivSubmodule R L M = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : 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>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>m : ↥(LieModule.maxTrivSubmodule R L M)<GOAL>↑((LieModule.maxTrivHom f) m) = f ↑m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : 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>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>e : M ≃ₗ⁅R,L⁆ N<VAR>m : ↥(LieModule.maxTrivSubmodule R L M)<GOAL>↑((LieModule.maxTrivEquiv e) m) = e ↑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<GOAL>LieModule.maxTrivEquiv LieModuleEquiv.refl = LieModuleEquiv.refl
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : 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>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>e : M ≃ₗ⁅R,L⁆ N<GOAL>(LieModule.maxTrivEquiv e).symm = LieModule.maxTrivEquiv e.symm
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : 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>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>f : ↥(LieModule.maxTrivSubmodule R L (M →ₗ[R] N))<GOAL>⇑(LieModule.maxTrivLinearMapEquivLieModuleHom f) = ⇑↑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : 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>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>⇑↑(LieModule.maxTrivLinearMapEquivLieModuleHom.symm f) = ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : 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>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>f : ↥(LieModule.maxTrivSubmodule R L (M →ₗ[R] N))<GOAL>↑(LieModule.maxTrivLinearMapEquivLieModuleHom f) = ↑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : 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>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>↑(LieModule.maxTrivLinearMapEquivLieModuleHom.symm f) = ↑f
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>(LieAlgebra.ad R L).ker = LieModule.ker R L L
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>LieModule.ker R L L = LieAlgebra.center R L
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>h : I ≤ LieAlgebra.center R L<GOAL>IsLieAbelian ↥↑I
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>IsLieAbelian L ↔ LieAlgebra.center R L = ⊤
<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>hx : x ∈ LieAlgebra.center R L<VAR>y : L<GOAL>Commute ((LieModule.toEnd R L M) x) ((LieModule.toEnd R L M) 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 : L<VAR>hx : x ∈ LieAlgebra.center R L<VAR>y : L<GOAL>Commute ((LieModule.toEnd R L M) y) ((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>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>LieModule.IsTrivial L M<GOAL>⁅I, N⁆ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>IsLieAbelian ↥↑I ↔ ⁅I, I⁆ = ⊥
<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>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>hN : IsAtom N<VAR>h : ⁅I, N⁆ ≠ ⊥<GOAL>⁅I, N⁆ = N
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>h : ¬IsLieAbelian ↥↑I<GOAL>⁅I, I⁆ = I
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>X Y : Matrix n n R<GOAL>⁅X, Y⁆.trace = 0
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>A B : ↥(LieAlgebra.SpecialLinear.sl n R)<GOAL>↑⁅A, B⁆ = ↑A * ↑B - ↑B * ↑A
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>i j : n<VAR>h : j ≠ i<GOAL>↑(LieAlgebra.SpecialLinear.Eb R i j h) = Matrix.stdBasisMatrix i j 1
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>Nontrivial R<VAR>h : 1 < Fintype.card n<GOAL>¬IsLieAbelian ↥(LieAlgebra.SpecialLinear.sl n R)
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>A : Matrix n n R<GOAL>A ∈ LieAlgebra.Orthogonal.so n R ↔ A.transpose = -A
<VAR>p : Type u_2<VAR>q : Type u_3<VAR>R : Type u₂<VAR>DecidableEq p<VAR>DecidableEq q<VAR>CommRing R<VAR>Fintype p<VAR>Fintype q<VAR>i : R<VAR>hi : i * i = -1<GOAL>LieAlgebra.Orthogonal.Pso p q R i * LieAlgebra.Orthogonal.Pso p q R (-i) = 1
<VAR>p : Type u_2<VAR>q : Type u_3<VAR>R : Type u₂<VAR>DecidableEq p<VAR>DecidableEq q<VAR>CommRing R<VAR>Fintype p<VAR>Fintype q<VAR>i : R<VAR>hi : i * i = -1<GOAL>(LieAlgebra.Orthogonal.Pso p q R i).transpose * LieAlgebra.Orthogonal.indefiniteDiagonal p q R * LieAlgebra.Orthogonal.Pso p q R i = 1
<VAR>p : Type u_2<VAR>q : Type u_3<VAR>R : Type u₂<VAR>DecidableEq p<VAR>DecidableEq q<VAR>CommRing R<VAR>Fintype p<VAR>Fintype q<VAR>i : R<VAR>hi : i * i = -1<VAR>A : ↥(LieAlgebra.Orthogonal.so' p q R)<GOAL>↑((LieAlgebra.Orthogonal.soIndefiniteEquiv p q R hi) A) = (LieAlgebra.Orthogonal.Pso p q R i)⁻¹ * ↑A * LieAlgebra.Orthogonal.Pso p q R i
<VAR>l : Type u_4<VAR>R : Type u₂<VAR>DecidableEq l<VAR>CommRing R<GOAL>LieAlgebra.Orthogonal.S l R = Matrix.fromBlocks 1 0 0 (-1)
<VAR>l : Type u_4<VAR>R : Type u₂<VAR>DecidableEq l<VAR>CommRing R<VAR>Fintype l<GOAL>(LieAlgebra.Orthogonal.PD l R).transpose * LieAlgebra.Orthogonal.JD l R * LieAlgebra.Orthogonal.PD l R = 2 • LieAlgebra.Orthogonal.S l R
<VAR>l : Type u_4<VAR>R : Type u₂<VAR>DecidableEq l<VAR>CommRing R<VAR>Fintype l<VAR>Invertible 2<GOAL>LieAlgebra.Orthogonal.PD l R * ⅟2 • (LieAlgebra.Orthogonal.PD l R).transpose = 1
<VAR>l : Type u_4<VAR>R : Type u₂<VAR>DecidableEq l<VAR>CommRing R<VAR>Fintype l<VAR>Invertible 2<GOAL>LieAlgebra.Orthogonal.PB l R * Matrix.fromBlocks 1 0 0 ⅟(LieAlgebra.Orthogonal.PD l R) = 1
<VAR>l : Type u_4<VAR>R : Type u₂<VAR>DecidableEq l<VAR>CommRing R<VAR>Fintype l<GOAL>(LieAlgebra.Orthogonal.PB l R).transpose * LieAlgebra.Orthogonal.JB l R * LieAlgebra.Orthogonal.PB l R = 2 • Matrix.fromBlocks 1 0 0 (LieAlgebra.Orthogonal.S l R)
<VAR>l : Type u_4<VAR>R : Type u₂<VAR>DecidableEq l<VAR>CommRing R<VAR>Fintype l<GOAL>LieAlgebra.Orthogonal.indefiniteDiagonal (Unit ⊕ l) l R = (Matrix.reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (Matrix.fromBlocks 1 0 0 (LieAlgebra.Orthogonal.indefiniteDiagonal l l R))
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>self : H.IsCartanSubalgebra<GOAL>H.normalizer = H
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>self : H.IsCartanSubalgebra<GOAL>LieAlgebra.IsNilpotent R ↥H
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>H.IsCartanSubalgebra<GOAL>H.toLieSubmodule.normalizer = H.toLieSubmodule
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>H.IsCartanSubalgebra<VAR>k : ℕ<GOAL>LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<GOAL>H.IsCartanSubalgebra ↔ H.toLieSubmodule.IsUcsLimit
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Nontrivial L<VAR>H : LieSubalgebra R L<VAR>H.IsCartanSubalgebra<GOAL>H ≠ ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>(lieIdealSubalgebra R L I).normalizer = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>a : L<GOAL>∀ (a_1 : L), ((LieDerivation.ad R L) a) a_1 = ⁅a, a_1⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : L<GOAL>↑((LieDerivation.ad R L) x) = (LieAlgebra.ad R L) x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : L<VAR>D : LieDerivation R L L<GOAL>(LieDerivation.ad R L) (D x) = -⁅x, D⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : L<VAR>D : LieDerivation R L L<GOAL>⁅(LieDerivation.ad R L) x, D⁆ = ⁅x, D⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>(LieDerivation.ad R L).ker = 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 : LieAlgebra.center R L = ⊥<GOAL>Function.Injective ⇑(LieDerivation.ad R L)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>D : LieDerivation R L L<VAR>x : L<GOAL>⁅D, (LieDerivation.ad R L) x⁆ = (LieDerivation.ad R L) (D x)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>(LieDerivation.ad R L).IsIdealMorphism
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>D : LieDerivation R L L<GOAL>D ∈ (LieDerivation.ad R L).idealRange ↔ ∃ x, (LieDerivation.ad R L) x = D
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>h : LieAlgebra.center R L = ⊥<GOAL>LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>f g : Module.End R M<VAR>hf : f ∈ LinearMap.skewAdjointSubmodule B<VAR>hg : g ∈ LinearMap.skewAdjointSubmodule B<GOAL>⁅f, g⁆ ∈ LinearMap.skewAdjointSubmodule B
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>N : Type w<VAR>AddCommGroup N<VAR>Module R N<VAR>e : N ≃ₗ[R] M<VAR>f : ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e))<GOAL>↑((skewAdjointLieSubalgebraEquiv B e) f) = e.lieConj ↑f
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>N : Type w<VAR>AddCommGroup N<VAR>Module R N<VAR>e : N ≃ₗ[R] M<VAR>f : ↥(skewAdjointLieSubalgebra B)<GOAL>↑((skewAdjointLieSubalgebraEquiv B e).symm f) = e.symm.lieConj ↑f
<VAR>R : Type u<VAR>n : Type w<VAR>CommRing R<VAR>DecidableEq n<VAR>Fintype n<VAR>A B : Matrix n n R<GOAL>⁅A, B⁆.transpose = ⁅B.transpose, A.transpose⁆
<VAR>R : Type u<VAR>n : Type w<VAR>CommRing R<VAR>DecidableEq n<VAR>Fintype n<VAR>J : Matrix n n R<VAR>A B : Matrix n n R<VAR>hA : A ∈ skewAdjointMatricesSubmodule J<VAR>hB : B ∈ skewAdjointMatricesSubmodule J<GOAL>⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J
<VAR>R : Type u<VAR>n : Type w<VAR>CommRing R<VAR>DecidableEq n<VAR>Fintype n<VAR>J A : Matrix n n R<GOAL>A ∈ skewAdjointMatricesLieSubalgebra J ↔ A ∈ skewAdjointMatricesSubmodule J
<VAR>R : Type u<VAR>n : Type w<VAR>CommRing R<VAR>DecidableEq n<VAR>Fintype n<VAR>J P : Matrix n n R<VAR>h : Invertible P<VAR>A : ↥(skewAdjointMatricesLieSubalgebra J)<GOAL>↑((skewAdjointMatricesLieSubalgebraEquiv J P h) A) = P⁻¹ * ↑A * P
<VAR>R : Type u<VAR>n : Type w<VAR>CommRing R<VAR>DecidableEq n<VAR>Fintype n<VAR>J : Matrix n n R<VAR>m : Type w<VAR>DecidableEq m<VAR>Fintype m<VAR>e : Matrix n n R ≃ₐ[R] Matrix m m R<VAR>h : ∀ (A : Matrix n n R), (e A).transpose = e A.transpose<VAR>A : ↥(skewAdjointMatricesLieSubalgebra J)<GOAL>↑((skewAdjointMatricesLieSubalgebraEquivTranspose J e h) A) = e ↑A
<VAR>R : Type u<VAR>n : Type w<VAR>CommRing R<VAR>DecidableEq n<VAR>Fintype n<VAR>u : Rˣ<VAR>J A : Matrix n n R<GOAL>A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J
<VAR>L : Type u_2<VAR>LieRing L<VAR>h e f : L<VAR>self : IsSl2Triple h e f<GOAL>⁅e, f⁆ = h
<VAR>L : Type u_2<VAR>LieRing L<VAR>h e f : L<VAR>self : IsSl2Triple h e f<GOAL>h ≠ 0
<VAR>L : Type u_2<VAR>LieRing L<VAR>h e f : L<VAR>self : IsSl2Triple h e f<GOAL>⁅h, e⁆ = 2 • e
<VAR>L : Type u_2<VAR>LieRing L<VAR>h e f : L<VAR>self : IsSl2Triple h e f<GOAL>⁅h, f⁆ = -(2 • f)
<VAR>L : Type u_2<VAR>LieRing L<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<GOAL>IsSl2Triple (-h) f e
<VAR>L : Type u_2<VAR>LieRing L<VAR>h e f : L<GOAL>IsSl2Triple (-h) f e ↔ IsSl2Triple h e f
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>h e f : L<VAR>t : IsSl2Triple h e f<GOAL>⁅h, e⁆ = 2 • e
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>h e f : L<VAR>t : IsSl2Triple h e f<GOAL>⁅h, f⁆ = -(2 • f)
<VAR>L : Type u_2<VAR>LieRing L<VAR>h e f : L<VAR>t : IsSl2Triple h e f<GOAL>e ≠ 0
<VAR>L : Type u_2<VAR>LieRing L<VAR>h e f : L<VAR>t : IsSl2Triple h e f<GOAL>f ≠ 0
<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>h e f : L<VAR>t : IsSl2Triple h e f<VAR>m : M<VAR>μ : R<VAR>self : t.HasPrimitiveVectorWith m μ<GOAL>⁅h, m⁆ = μ • 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>h e f : L<VAR>t : IsSl2Triple h e f<VAR>m : M<VAR>μ : R<VAR>self : t.HasPrimitiveVectorWith m μ<GOAL>m ≠ 0
<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>h e f : L<VAR>t : IsSl2Triple h e f<VAR>m : M<VAR>μ : R<VAR>self : t.HasPrimitiveVectorWith m μ<GOAL>⁅e, m⁆ = 0
<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>LieModule R L M<VAR>h e f : L<VAR>NoZeroSMulDivisors ℤ M<VAR>t : IsSl2Triple h e f<VAR>m : M<VAR>μ ρ : R<VAR>hm : m ≠ 0<VAR>hm' : ⁅h, m⁆ = μ • m<VAR>he : ⁅e, m⁆ = ρ • m<GOAL>t.HasPrimitiveVectorWith m μ
<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>LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>n : ℕ<GOAL>⁅h, ((LieModule.toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((LieModule.toEnd R L M) f ^ n) m
<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>LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>n : ℕ<GOAL>⁅f, ((LieModule.toEnd R L M) f ^ n) m⁆ = ((LieModule.toEnd R L M) f ^ (n + 1)) m
<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>LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>n : ℕ<GOAL>⁅e, ((LieModule.toEnd R L M) f ^ (n + 1)) m⁆ = ((↑n + 1) * (μ - ↑n)) • ((LieModule.toEnd R L M) f ^ n) m
<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>LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>IsNoetherian R M<VAR>NoZeroSMulDivisors R M<VAR>IsDomain R<VAR>CharZero R<GOAL>∃ n, μ = ↑n
<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>LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>CharZero R<VAR>NoZeroSMulDivisors R M<VAR>n : ℕ<VAR>hn : μ = ↑n<VAR>i : ℕ<VAR>hi : i ≤ n<GOAL>((LieModule.toEnd R L M) f ^ i) m ≠ 0
<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>LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>IsNoetherian R M<VAR>NoZeroSMulDivisors R M<VAR>IsDomain R<VAR>CharZero R<VAR>n : ℕ<VAR>hn : μ = ↑n<GOAL>((LieModule.toEnd R L M) f ^ (n + 1)) m = 0
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>∀ (a : L), (UniversalEnvelopingAlgebra.ι R) a = (UniversalEnvelopingAlgebra.mkAlgHom R L) (ιₜ a)
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>A : Type u₃<VAR>Ring A<VAR>Algebra R A<VAR>F : UniversalEnvelopingAlgebra R L →ₐ[R] A<GOAL>(UniversalEnvelopingAlgebra.lift R).symm F = F.toLieHom.comp (UniversalEnvelopingAlgebra.ι R)
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>A : Type u₃<VAR>Ring A<VAR>Algebra R A<VAR>f : L →ₗ⁅R⁆ A<GOAL>⇑((UniversalEnvelopingAlgebra.lift R) f) ∘ ⇑(UniversalEnvelopingAlgebra.ι R) = ⇑f
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>A : Type u₃<VAR>Ring A<VAR>Algebra R A<VAR>f : L →ₗ⁅R⁆ A<VAR>x : L<GOAL>((UniversalEnvelopingAlgebra.lift R) f) ((UniversalEnvelopingAlgebra.ι R) x) = f x
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>A : Type u₃<VAR>Ring A<VAR>Algebra R A<VAR>f : L →ₗ⁅R⁆ A<VAR>x : L<GOAL>((UniversalEnvelopingAlgebra.lift R) f) ((UniversalEnvelopingAlgebra.mkAlgHom R L) (ιₜ x)) = f x
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>A : Type u₃<VAR>Ring A<VAR>Algebra R A<VAR>f : L →ₗ⁅R⁆ A<VAR>g : UniversalEnvelopingAlgebra R L →ₐ[R] A<GOAL>⇑g ∘ ⇑(UniversalEnvelopingAlgebra.ι R) = ⇑f ↔ g = (UniversalEnvelopingAlgebra.lift R) f
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>A : Type u₃<VAR>Ring A<VAR>Algebra R A<VAR>g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A<VAR>h : g₁.toLieHom.comp (UniversalEnvelopingAlgebra.ι R) = g₂.toLieHom.comp (UniversalEnvelopingAlgebra.ι R)<GOAL>g₁ = g₂
<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 η ε = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.Bicategory.rightUnitor f).inv<GOAL>CategoryTheory.bicategoricalComp (CategoryTheory.Bicategory.rightZigzag η ε) (CategoryTheory.Bicategory.rightZigzag η ε) = CategoryTheory.Bicategory.rightZigzag η ε
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>self : CategoryTheory.Bicategory.Adjunction f g<GOAL>CategoryTheory.Bicategory.leftZigzag self.unit self.counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.Bicategory.rightUnitor f).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>self : CategoryTheory.Bicategory.Adjunction f g<GOAL>CategoryTheory.Bicategory.rightZigzag self.unit self.counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom (CategoryTheory.Bicategory.leftUnitor g).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f₁ : a ⟶ b<VAR>g₁ : b ⟶ a<VAR>f₂ : b ⟶ c<VAR>g₂ : c ⟶ b<VAR>adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁<VAR>adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂<GOAL>CategoryTheory.Bicategory.leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f₁ f₂)).hom (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f₁ f₂)).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f₁ : a ⟶ b<VAR>g₁ : b ⟶ a<VAR>f₂ : b ⟶ c<VAR>g₂ : c ⟶ b<VAR>adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁<VAR>adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂<GOAL>CategoryTheory.Bicategory.rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp g₂ g₁)).hom (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp g₂ g₁)).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f₁ : a ⟶ b<VAR>g₁ : b ⟶ a<VAR>f₂ : b ⟶ c<VAR>g₂ : c ⟶ b<VAR>adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁<VAR>adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂<GOAL>(adj₁.comp adj₂).unit = adj₁.compUnit adj₂
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f₁ : a ⟶ b<VAR>g₁ : b ⟶ a<VAR>f₂ : b ⟶ c<VAR>g₂ : c ⟶ b<VAR>adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁<VAR>adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂<GOAL>(adj₁.comp adj₂).counit = adj₁.compCounit adj₂
<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 η ε).hom = CategoryTheory.Bicategory.leftZigzag η.hom ε.hom
<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 η ε).hom = CategoryTheory.Bicategory.rightZigzag η.hom ε.hom
<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 η ε).inv = CategoryTheory.Bicategory.rightZigzag ε.inv η.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.rightZigzagIso η ε).inv = CategoryTheory.Bicategory.leftZigzag ε.inv η.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 η ε).symm = CategoryTheory.Bicategory.rightZigzagIso ε.symm η.symm