ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>AddSemigroup R<VAR>a b : R<GOAL>IsAddRegular (a + b) ∧ IsAddRegular (b + a) ↔ IsAddRegular a ∧ IsAddRegular b
<VAR>R : Type u_1<VAR>Semigroup R<VAR>a b : R<GOAL>IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b
<VAR>R : Type u_1<VAR>Semigroup R<VAR>a b : R<VAR>ab : IsRegular (a * b)<VAR>ba : IsRegular (b * a)<GOAL>IsRegular a ∧ IsRegular b
<VAR>R : Type u_1<VAR>AddSemigroup R<VAR>a b : R<VAR>ab : IsAddRegular (a + b)<VAR>ba : IsAddRegular (b + a)<GOAL>IsAddRegular a ∧ IsAddRegular b
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>h : IsLeftRegular 0<GOAL>Subsingleton R
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>h : IsRightRegular 0<GOAL>Subsingleton R
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>h : IsRegular 0<GOAL>Subsingleton R
<VAR>R : Type u_1<VAR>MulZeroClass R<GOAL>IsLeftRegular 0 ↔ Subsingleton R
<VAR>R : Type u_1<VAR>MulZeroClass R<GOAL>¬IsLeftRegular 0 ↔ Nontrivial R
<VAR>R : Type u_1<VAR>MulZeroClass R<GOAL>IsRightRegular 0 ↔ Subsingleton R
<VAR>R : Type u_1<VAR>MulZeroClass R<GOAL>¬IsRightRegular 0 ↔ Nontrivial R
<VAR>R : Type u_1<VAR>MulZeroClass R<GOAL>IsRegular 0 ↔ Subsingleton R
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>a : R<VAR>Nontrivial R<VAR>la : IsLeftRegular a<GOAL>a ≠ 0
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>a : R<VAR>Nontrivial R<VAR>ra : IsRightRegular a<GOAL>a ≠ 0
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>a : R<VAR>Nontrivial R<VAR>la : IsRegular a<GOAL>a ≠ 0
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>nR : Nontrivial R<GOAL>¬IsLeftRegular 0
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>nR : Nontrivial R<GOAL>¬IsRightRegular 0
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>Nontrivial R<GOAL>¬IsRegular 0
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>a b : R<VAR>hb : IsLeftRegular b<GOAL>b * a = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>a b : R<VAR>hb : IsRightRegular b<GOAL>a * b = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>AddZeroClass R<GOAL>IsAddRegular 0
<VAR>R : Type u_1<VAR>MulOneClass R<GOAL>IsRegular 1
<VAR>R : Type u_1<VAR>AddCommSemigroup R<VAR>a b : R<GOAL>IsAddRegular (a + b) ↔ IsAddRegular a ∧ IsAddRegular b
<VAR>R : Type u_1<VAR>CommSemigroup R<VAR>a b : R<GOAL>IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b
<VAR>R : Type u_1<VAR>Monoid R<VAR>a b : R<VAR>h : b * a = 1<GOAL>IsLeftRegular a
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>a b : R<VAR>h : b + a = 0<GOAL>IsAddLeftRegular a
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>a b : R<VAR>h : a + b = 0<GOAL>IsAddRightRegular a
<VAR>R : Type u_1<VAR>Monoid R<VAR>a b : R<VAR>h : a * b = 1<GOAL>IsRightRegular a
<VAR>R : Type u_1<VAR>Monoid R<VAR>a : Rˣ<GOAL>IsRegular ↑a
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>a : AddUnits R<GOAL>IsAddRegular ↑a
<VAR>R : Type u_1<VAR>Monoid R<VAR>a : R<VAR>ua : IsUnit a<GOAL>IsRegular a
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>a : R<VAR>ua : IsAddUnit a<GOAL>IsAddRegular a
<VAR>R : Type u_1<VAR>Mul R<VAR>IsLeftCancelMul R<VAR>g : R<GOAL>IsLeftRegular g
<VAR>R : Type u_1<VAR>Add R<VAR>IsLeftCancelAdd R<VAR>g : R<GOAL>IsAddLeftRegular g
<VAR>R : Type u_1<VAR>Add R<VAR>IsRightCancelAdd R<VAR>g : R<GOAL>IsAddRightRegular g
<VAR>R : Type u_1<VAR>Mul R<VAR>IsRightCancelMul R<VAR>g : R<GOAL>IsRightRegular g
<VAR>R : Type u_1<VAR>Add R<VAR>IsCancelAdd R<VAR>g : R<GOAL>IsAddRegular g
<VAR>R : Type u_1<VAR>Mul R<VAR>IsCancelMul R<VAR>g : R<GOAL>IsRegular g
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>IsCancelMulZero R<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>IsRegular a
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>IsCancelMulZero R<VAR>a : R<VAR>Nontrivial R<GOAL>IsRegular a ↔ a ≠ 0
<VAR>R : Type u_1<VAR>a : R<VAR>Monoid R<VAR>n : ℕ<VAR>rla : IsLeftRegular a<GOAL>IsLeftRegular (a ^ n)
<VAR>R : Type u_1<VAR>a : R<VAR>Monoid R<VAR>n : ℕ<VAR>rra : IsRightRegular a<GOAL>IsRightRegular (a ^ n)
<VAR>R : Type u_1<VAR>a : R<VAR>Monoid R<VAR>n : ℕ<VAR>ra : IsRegular a<GOAL>IsRegular (a ^ n)
<VAR>R : Type u_1<VAR>a : R<VAR>Monoid R<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsLeftRegular (a ^ n) ↔ IsLeftRegular a
<VAR>R : Type u_1<VAR>a : R<VAR>Monoid R<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsRightRegular (a ^ n) ↔ IsRightRegular a
<VAR>R : Type u_1<VAR>a : R<VAR>Monoid R<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsRegular (a ^ n) ↔ IsRegular a
<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>CommMonoid R<VAR>s : Finset ι<VAR>f : ι → R<VAR>h : ∀ i ∈ s, IsLeftRegular (f i)<GOAL>IsLeftRegular (∏ i ∈ s, f i)
<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>CommMonoid R<VAR>s : Finset ι<VAR>f : ι → R<VAR>h : ∀ i ∈ s, IsRightRegular (f i)<GOAL>IsRightRegular (∏ i ∈ s, f i)
<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>CommMonoid R<VAR>s : Finset ι<VAR>f : ι → R<VAR>h : ∀ i ∈ s, IsRegular (f i)<GOAL>IsRegular (∏ i ∈ s, f i)
<VAR>R : Type u_1<VAR>Mul R<VAR>c : R<VAR>h : IsLeftRegular c<GOAL>IsSMulRegular R c
<VAR>R : Type u_1<VAR>Mul R<VAR>a : R<GOAL>IsLeftRegular a ↔ IsSMulRegular R a
<VAR>R : Type u_1<VAR>Mul R<VAR>c : R<VAR>h : IsRightRegular c<GOAL>IsSMulRegular R (MulOpposite.op c)
<VAR>R : Type u_1<VAR>Mul R<VAR>a : R<GOAL>IsRightRegular a ↔ IsSMulRegular R (MulOpposite.op a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a : R<VAR>s : S<VAR>SMul R M<VAR>SMul R S<VAR>SMul S M<VAR>IsScalarTower R S M<VAR>ra : IsSMulRegular M a<VAR>rs : IsSMulRegular M s<GOAL>IsSMulRegular M (a • s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>s : S<VAR>SMul R M<VAR>SMul R S<VAR>SMul S M<VAR>IsScalarTower R S M<VAR>a : R<VAR>ab : IsSMulRegular M (a • s)<GOAL>IsSMulRegular M s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a : R<VAR>SMul R M<VAR>SMul R S<VAR>SMul S M<VAR>IsScalarTower R S M<VAR>b : S<VAR>ha : IsSMulRegular M a<GOAL>IsSMulRegular M (a • b) ↔ IsSMulRegular M b
<VAR>R : Type u_1<VAR>Mul R<VAR>a : R<VAR>h : IsSMulRegular R a<GOAL>IsLeftRegular a
<VAR>R : Type u_1<VAR>Mul R<VAR>a : R<VAR>h : IsSMulRegular R (MulOpposite.op a)<GOAL>IsRightRegular a
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>a b : R<VAR>SMul R M<VAR>Mul R<VAR>IsScalarTower R R M<VAR>ra : IsSMulRegular M a<VAR>rb : IsSMulRegular M b<GOAL>IsSMulRegular M (a * b)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>a b : R<VAR>SMul R M<VAR>Mul R<VAR>IsScalarTower R R M<VAR>ab : IsSMulRegular M (a * b)<GOAL>IsSMulRegular M b
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>a b : R<VAR>SMul R M<VAR>Mul R<VAR>IsScalarTower R R M<VAR>ha : IsSMulRegular M a<GOAL>IsSMulRegular M (a * b) ↔ IsSMulRegular M b
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>a b : R<VAR>SMul R M<VAR>Mul R<VAR>IsScalarTower R R M<GOAL>IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>SMul R M<VAR>N : Type u_4<VAR>F : Type u_5<VAR>SMul R N<VAR>FunLike F M N<VAR>MulActionHomClass F R M N<VAR>f : F<VAR>r : R<VAR>h1 : Function.Injective ⇑f<VAR>h2 : IsSMulRegular N r<GOAL>IsSMulRegular M r
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Monoid R<VAR>MulAction R M<GOAL>IsSMulRegular M 1
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>a b : R<VAR>Monoid R<VAR>MulAction R M<VAR>h : a * b = 1<GOAL>IsSMulRegular M b
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>a : R<VAR>Monoid R<VAR>MulAction R M<VAR>n : ℕ<VAR>ra : IsSMulRegular M a<GOAL>IsSMulRegular M (a ^ n)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>a : R<VAR>Monoid R<VAR>MulAction R M<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a : R<VAR>s : S<VAR>Monoid S<VAR>SMul R M<VAR>SMul R S<VAR>MulAction S M<VAR>IsScalarTower R S M<VAR>h : a • s = 1<GOAL>IsSMulRegular M s
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<VAR>h : IsSMulRegular M 0<GOAL>Subsingleton M
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<GOAL>IsSMulRegular M 0 ↔ Subsingleton M
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<GOAL>¬IsSMulRegular M 0 ↔ Nontrivial M
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<VAR>sM : Subsingleton M<GOAL>IsSMulRegular M 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<VAR>nM : Nontrivial M<GOAL>¬IsSMulRegular M 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>a b : R<VAR>CommSemigroup R<VAR>SMul R M<VAR>IsScalarTower R R M<GOAL>IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
<VAR>R : Type u_1<VAR>G : Type u_4<VAR>Group G<VAR>MulAction G R<VAR>g : G<GOAL>IsSMulRegular R g
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Monoid R<VAR>MulAction R M<VAR>a : Rˣ<GOAL>IsSMulRegular M ↑a
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>a : R<VAR>Monoid R<VAR>MulAction R M<VAR>ua : IsUnit a<GOAL>IsSMulRegular M a
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Zero M<VAR>SMulZeroClass R M<VAR>r : R<VAR>x : M<VAR>h1 : IsSMulRegular M r<VAR>h2 : r • x = 0<GOAL>x = 0
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>SMul R M<VAR>SMul S M'<VAR>e : M ≃ M'<VAR>r : R<VAR>s : S<VAR>h : ∀ (x : M), e (r • x) = s • e x<GOAL>IsSMulRegular M r ↔ IsSMulRegular M' s
<VAR>L : Type v<VAR>self : LieRing L<VAR>x y z : L<GOAL>⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
<VAR>L : Type v<VAR>self : LieRing L<VAR>x : L<GOAL>⁅x, x⁆ = 0
<VAR>L : Type v<VAR>self : LieRing L<VAR>x y z : L<GOAL>⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
<VAR>L : Type v<VAR>self : LieRing L<VAR>x y z : L<GOAL>⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>self : LieAlgebra R L<VAR>t : R<VAR>x y : L<GOAL>⁅x, t • y⁆ = t • ⁅x, y⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>self : LieRingModule L M<VAR>x y : L<VAR>m : M<GOAL>⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>self : LieRingModule L M<VAR>x y : L<VAR>m : M<GOAL>⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>self : LieRingModule L M<VAR>x : L<VAR>m n : M<GOAL>⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, 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>self : LieModule R L M<VAR>t : R<VAR>x : L<VAR>m : M<GOAL>⁅x, t • m⁆ = t • ⁅x, 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>self : LieModule R L M<VAR>t : R<VAR>x : L<VAR>m : M<GOAL>⁅t • x, m⁆ = t • ⁅x, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x y : L<VAR>m : M<GOAL>⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x : L<VAR>m n : M<GOAL>⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, 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>t : R<VAR>x : L<VAR>m : M<GOAL>⁅t • x, m⁆ = t • ⁅x, 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>t : R<VAR>x : L<VAR>m : M<GOAL>⁅x, t • m⁆ = t • ⁅x, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x y : L<VAR>m : M<GOAL>⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x : L<GOAL>⁅x, 0⁆ = 0
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>m : M<GOAL>⁅0, m⁆ = 0
<VAR>L : Type v<VAR>LieRing L<VAR>x : L<GOAL>⁅x, x⁆ = 0
<VAR>L : Type v<VAR>LieRing L<VAR>x y : L<GOAL>-⁅y, x⁆ = ⁅x, y⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x : L<VAR>m : M<GOAL>⁅-x, m⁆ = -⁅x, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x : L<VAR>m : M<GOAL>⁅x, -m⁆ = -⁅x, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x y : L<VAR>m : M<GOAL>⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x : L<VAR>m n : M<GOAL>⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x : L<VAR>m : M<VAR>n : ℕ<GOAL>⁅n • x, m⁆ = n • ⁅x, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x : L<VAR>m : M<VAR>n : ℕ<GOAL>⁅x, n • m⁆ = n • ⁅x, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x : L<VAR>m : M<VAR>a : ℤ<GOAL>⁅a • x, m⁆ = a • ⁅x, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x : L<VAR>m : M<VAR>a : ℤ<GOAL>⁅x, a • m⁆ = a • ⁅x, m⁆
<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x y : L<VAR>m : M<GOAL>⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
<VAR>L : Type v<VAR>LieRing L<VAR>x y z : L<GOAL>⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0
<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] N<VAR>x : L<VAR>m : M<GOAL>⁅x, f⁆ m = ⁅x, f m⁆ - f ⁅x, 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>x : L<VAR>m : M<VAR>f : M →ₗ[R] R<GOAL>⁅x, f⁆ m = -f ⁅x, m⁆
<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>self : L →ₗ⁅R⁆ L'<VAR>x y : L<GOAL>(↑self).toFun ⁅x, y⁆ = ⁅(↑self).toFun x, (↑self).toFun y⁆
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<GOAL>⇑↑f = ⇑f
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<GOAL>(↑f).toFun = ⇑f
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>c : R<VAR>x : L₁<GOAL>f (c • x) = c • f x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>x y : L₁<GOAL>f (x + y) = f x + f y
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>x y : L₁<GOAL>f (x - y) = f x - f y
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>x : L₁<GOAL>f (-x) = -f x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>x y : L₁<GOAL>f ⁅x, y⁆ = ⁅f x, f y⁆
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<GOAL>f 0 = 0
<VAR>R : Type u<VAR>L₁ : Type v<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<GOAL>⇑LieHom.id = id
<VAR>R : Type u<VAR>L₁ : Type v<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>x : L₁<GOAL>LieHom.id x = x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<GOAL>⇑0 = 0
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>x : L₁<GOAL>0 x = 0
<VAR>R : Type u<VAR>L₁ : Type v<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<GOAL>⇑1 = id
<VAR>R : Type u<VAR>L₁ : Type v<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>x : L₁<GOAL>1 x = x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<GOAL>Function.Injective DFunLike.coe
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f g : L₁ →ₗ⁅R⁆ L₂<VAR>h : ∀ (x : L₁), f x = g x<GOAL>f = g
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f g : L₁ →ₗ⁅R⁆ L₂<GOAL>f = g ↔ ∀ (x : L₁), f x = g x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f g : L₁ →ₗ⁅R⁆ L₂<VAR>h : f = g<VAR>x : L₁<GOAL>f x = g x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>h₁ : ∀ (x y : L₁), f (x + y) = f x + f y<VAR>h₂ : ∀ (m : R) (x : L₁), { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x<VAR>h₃ : ∀ {x y : L₁}, { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ = ⁅{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun x, { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆<GOAL>{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ → L₂<VAR>h₁ : ∀ (x y : L₁), f (x + y) = f x + f y<VAR>h₂ : ∀ (m : R) (x : L₁), { toFun := f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h₁ }.toFun x<VAR>h₃ : ∀ {x y : L₁}, { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ = ⁅{ toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun x, { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆<GOAL>⇑{ toFun := f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>L₃ : Type w₁<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>LieRing L₃<VAR>LieAlgebra R L₃<VAR>f : L₂ →ₗ⁅R⁆ L₃<VAR>g : L₁ →ₗ⁅R⁆ L₂<VAR>x : L₁<GOAL>(f.comp g) x = f (g x)
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>L₃ : Type w₁<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>LieRing L₃<VAR>LieAlgebra R L₃<VAR>f : L₂ →ₗ⁅R⁆ L₃<VAR>g : L₁ →ₗ⁅R⁆ L₂<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>L₃ : Type w₁<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>LieRing L₃<VAR>LieAlgebra R L₃<VAR>f : L₂ →ₗ⁅R⁆ L₃<VAR>g : L₁ →ₗ⁅R⁆ L₂<GOAL>↑(f.comp g) = ↑f ∘ₗ ↑g
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<GOAL>f.comp LieHom.id = f
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<GOAL>LieHom.id.comp f = f
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>M : Type w₁<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>AddCommGroup M<VAR>LieRingModule L₂ M<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>x : L₁<VAR>m : M<GOAL>⁅x, m⁆ = ⁅f x, m⁆
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>M : Type w₁<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>AddCommGroup M<VAR>LieRingModule L₂ M<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>Module R M<VAR>LieModule R L₂ M<GOAL>LieModule R L₁ M
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>self : L ≃ₗ⁅R⁆ L'<GOAL>Function.LeftInverse self.invFun (↑self.toLieHom).toFun
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>self : L ≃ₗ⁅R⁆ L'<GOAL>Function.RightInverse self.invFun (↑self.toLieHom).toFun
<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>⇑e.toLieHom = ⇑e
<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>⇑e.toLinearEquiv = ⇑e
<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>g : L₂ → L₁<VAR>h₁ : Function.LeftInverse g (↑f).toFun<VAR>h₂ : Function.RightInverse g (↑f).toFun<GOAL>{ toLieHom := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toLinearEquiv = { toLinearMap := ↑f, invFun := g, left_inv := h₁, right_inv := h₂ }
<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₂<GOAL>Function.Injective LieEquiv.toLinearEquiv
<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₂<GOAL>Function.Injective DFunLike.coe
<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 g : L₁ ≃ₗ⁅R⁆ L₂<VAR>h : ∀ (x : L₁), f x = g x<GOAL>f = g
<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₂<VAR>x y : L₁<GOAL>e ⁅x, y⁆ = ⁅e x, e y⁆
<VAR>R : Type u<VAR>L₁ : Type v<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>x : L₁<GOAL>LieEquiv.refl x = x
<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>e.symm.symm = e
<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₂<GOAL>Function.Bijective LieEquiv.symm
<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₂<VAR>x : L₂<GOAL>e (e.symm x) = x
<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₂<VAR>x : L₁<GOAL>e.symm (e x) = x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<GOAL>LieEquiv.refl.symm = LieEquiv.refl
<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>e.trans e.symm = LieEquiv.refl
<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>e.symm.trans e = LieEquiv.refl
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>L₃ : Type w₁<VAR>CommRing R<VAR>LieRing L₁<VAR>LieRing L₂<VAR>LieRing L₃<VAR>LieAlgebra R L₁<VAR>LieAlgebra R L₂<VAR>LieAlgebra R L₃<VAR>e₁ : L₁ ≃ₗ⁅R⁆ L₂<VAR>e₂ : L₂ ≃ₗ⁅R⁆ L₃<VAR>x : L₁<GOAL>(e₁.trans e₂) x = e₂ (e₁ x)
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>L₃ : Type w₁<VAR>CommRing R<VAR>LieRing L₁<VAR>LieRing L₂<VAR>LieRing L₃<VAR>LieAlgebra R L₁<VAR>LieAlgebra R L₂<VAR>LieAlgebra R L₃<VAR>e₁ : L₁ ≃ₗ⁅R⁆ L₂<VAR>e₂ : L₂ ≃ₗ⁅R⁆ L₃<GOAL>(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
<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>Function.Bijective ⇑e.toLieHom
<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>Function.Injective ⇑e.toLieHom
<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>Function.Surjective ⇑e.toLieHom
<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.Bijective ⇑f<VAR>a : L₁<GOAL>(LieEquiv.ofBijective f h) a = f a
<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.Bijective ⇑f<GOAL>∀ (a : L₂), (LieEquiv.ofBijective f h).invFun a = (LinearEquiv.ofBijective (↑f) h).symm a