ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a : R<GOAL>EuclideanDomain.gcd 1 a = 1
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a : R<GOAL>EuclideanDomain.gcd a a = a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x y s t s' t' : R<GOAL>(EuclideanDomain.xgcdAux x s t y s' t').1 = EuclideanDomain.gcd x y
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x y : R<GOAL>EuclideanDomain.xgcdAux x 1 0 y 0 1 = (EuclideanDomain.gcd x y, EuclideanDomain.xgcd x y)
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a b : R<VAR>r r' s t s' t' : R<VAR>p : EuclideanDomain.P a b (r, s, t)<VAR>p' : EuclideanDomain.P a b (r', s', t')<GOAL>EuclideanDomain.P a b (EuclideanDomain.xgcdAux r s t r' s' t')
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a b : R<GOAL>EuclideanDomain.gcd a b = a * EuclideanDomain.gcdA a b + b * EuclideanDomain.gcdB a b
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x y : R<GOAL>x ∣ EuclideanDomain.lcm x y
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x y : R<GOAL>y ∣ EuclideanDomain.lcm x y
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x y z : R<VAR>hxz : x ∣ z<VAR>hyz : y ∣ z<GOAL>EuclideanDomain.lcm x y ∣ z
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x y z : R<GOAL>EuclideanDomain.lcm x y ∣ z ↔ x ∣ z ∧ y ∣ z
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x : R<GOAL>EuclideanDomain.lcm 0 x = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x : R<GOAL>EuclideanDomain.lcm x 0 = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x y : R<GOAL>EuclideanDomain.lcm x y = 0 ↔ x = 0 ∨ y = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x y : R<GOAL>EuclideanDomain.gcd x y * EuclideanDomain.lcm x y = x * y
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>hcb : c ∣ b<GOAL>a * b / (a * c) = b / c
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b c d : R<VAR>hac : c ∣ a<VAR>hbd : d ∣ b<GOAL>a * b / (c * d) = a / c * (b / d)
<VAR>R : Type u<VAR>X : Type v<VAR>Semiring R<VAR>A : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A<GOAL>(FreeNonUnitalNonAssocAlgebra.lift R).symm F = ⇑F ∘ FreeNonUnitalNonAssocAlgebra.of R
<VAR>R : Type u<VAR>X : Type v<VAR>Semiring R<VAR>A : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>f : X → A<GOAL>⇑((FreeNonUnitalNonAssocAlgebra.lift R) f) ∘ FreeNonUnitalNonAssocAlgebra.of R = f
<VAR>R : Type u<VAR>X : Type v<VAR>Semiring R<VAR>A : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>f : X → A<VAR>F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A<GOAL>⇑F ∘ FreeNonUnitalNonAssocAlgebra.of R = f ↔ F = (FreeNonUnitalNonAssocAlgebra.lift R) f
<VAR>R : Type u<VAR>X : Type v<VAR>Semiring R<VAR>A : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>f : X → A<VAR>x : X<GOAL>((FreeNonUnitalNonAssocAlgebra.lift R) f) (FreeNonUnitalNonAssocAlgebra.of R x) = f x
<VAR>R : Type u<VAR>X : Type v<VAR>Semiring R<VAR>A : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A<GOAL>(FreeNonUnitalNonAssocAlgebra.lift R) (⇑F ∘ FreeNonUnitalNonAssocAlgebra.of R) = F
<VAR>R : Type u<VAR>X : Type v<VAR>Semiring R<VAR>A : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>F₁ F₂ : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A<VAR>h : ∀ (x : X), F₁ (FreeNonUnitalNonAssocAlgebra.of R x) = F₂ (FreeNonUnitalNonAssocAlgebra.of R x)<GOAL>F₁ = F₂
<VAR>α : Type u_1<VAR>CommSemiring α<VAR>E : LinearRecurrence α<VAR>init : Fin E.order → α<GOAL>E.IsSolution (E.mkSol init)
<VAR>α : Type u_1<VAR>CommSemiring α<VAR>E : LinearRecurrence α<VAR>init : Fin E.order → α<VAR>n : Fin E.order<GOAL>E.mkSol init ↑n = init n
<VAR>α : Type u_1<VAR>CommSemiring α<VAR>E : LinearRecurrence α<VAR>u : ℕ → α<VAR>init : Fin E.order → α<VAR>h : E.IsSolution u<VAR>heq : ∀ (n : Fin E.order), u ↑n = init n<VAR>n : ℕ<GOAL>u n = E.mkSol init n
<VAR>α : Type u_1<VAR>CommSemiring α<VAR>E : LinearRecurrence α<VAR>u : ℕ → α<VAR>init : Fin E.order → α<VAR>h : E.IsSolution u<VAR>heq : ∀ (n : Fin E.order), u ↑n = init n<GOAL>u = E.mkSol init
<VAR>α : Type u_1<VAR>CommSemiring α<VAR>E : LinearRecurrence α<VAR>u : ℕ → α<GOAL>E.IsSolution u ↔ u ∈ E.solSpace
<VAR>α : Type u_1<VAR>CommSemiring α<VAR>E : LinearRecurrence α<VAR>u v : ℕ → α<VAR>hu : E.IsSolution u<VAR>hv : E.IsSolution v<GOAL>u = v ↔ Set.EqOn u v ↑(Finset.range E.order)
<VAR>α : Type u_1<VAR>CommRing α<VAR>StrongRankCondition α<VAR>E : LinearRecurrence α<GOAL>Module.rank α ↥E.solSpace = ↑E.order
<VAR>α : Type u_1<VAR>CommRing α<VAR>E : LinearRecurrence α<VAR>q : α<GOAL>(E.IsSolution fun n => q ^ n) ↔ E.charPoly.IsRoot q
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c d : G₀<VAR>hbd : Commute b d<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<GOAL>a / b = c / d ↔ a * d = c * b
<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>F : Type u_6<VAR>MonoidWithZero M₀<VAR>GroupWithZero G₀<VAR>Nontrivial M₀<VAR>FunLike F G₀ M₀<VAR>MonoidWithZeroHomClass F G₀ M₀<VAR>f : F<VAR>a : G₀<GOAL>f a ≠ 0 ↔ a ≠ 0
<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>F : Type u_6<VAR>MonoidWithZero M₀<VAR>GroupWithZero G₀<VAR>Nontrivial M₀<VAR>FunLike F G₀ M₀<VAR>MonoidWithZeroHomClass F G₀ M₀<VAR>f : F<VAR>a : G₀<GOAL>f a = 0 ↔ a = 0
<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>F' : Type u_7<VAR>GroupWithZero G₀<VAR>MonoidWithZero M₀'<VAR>FunLike F' G₀ M₀'<VAR>a : G₀<VAR>MonoidWithZeroHomClass F' G₀ M₀'<VAR>f g : F'<VAR>h : f a = g a<GOAL>f a⁻¹ = g a⁻¹
<VAR>G₀ : Type u_3<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>GroupWithZero G₀<VAR>GroupWithZero G₀'<VAR>FunLike F G₀ G₀'<VAR>MonoidWithZeroHomClass F G₀ G₀'<VAR>f : F<VAR>a : G₀<GOAL>f a⁻¹ = (f a)⁻¹
<VAR>G₀ : Type u_3<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>GroupWithZero G₀<VAR>GroupWithZero G₀'<VAR>FunLike F G₀ G₀'<VAR>MonoidWithZeroHomClass F G₀ G₀'<VAR>f : F<VAR>a b : G₀<GOAL>f (a / b) = f a / f b
<VAR>M : Type u_8<VAR>CommMonoidWithZero M<GOAL>⇑MonoidWithZero.inverse = Ring.inverse
<VAR>M : Type u_8<VAR>CommMonoidWithZero M<VAR>a : M<GOAL>MonoidWithZero.inverse a = Ring.inverse a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>α : Type u_8<VAR>SMul G₀ α<VAR>g : G₀<VAR>hg : g ≠ 0<VAR>a : α<GOAL>Units.mk0 g hg • a = g • a
<VAR>F : Type u_8<VAR>G₀ : Type u_9<VAR>G₀' : Type u_10<VAR>GroupWithZero G₀<VAR>GroupWithZero G₀'<VAR>FunLike F G₀ G₀'<VAR>MonoidWithZeroHomClass F G₀ G₀'<VAR>f : F<VAR>x : G₀<VAR>n : ℤ<GOAL>f (x ^ n) = f x ^ n
<VAR>α : Type u_1<VAR>GroupWithZero α<VAR>a b : α<GOAL>IsConj a b ↔ ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b
<VAR>G : Type u_1<VAR>GroupWithZero G<VAR>a : G<VAR>ha : a ≠ 0<GOAL>⇑(Equiv.mulLeft₀ a ha) = fun x => a * x
<VAR>G : Type u_1<VAR>GroupWithZero G<VAR>a : G<VAR>ha : a ≠ 0<GOAL>⇑(Equiv.symm (Equiv.mulLeft₀ a ha)) = fun x => a⁻¹ * x
<VAR>G : Type u_1<VAR>GroupWithZero G<VAR>a : G<VAR>ha : a ≠ 0<GOAL>Function.Bijective fun x => a * x
<VAR>G : Type u_1<VAR>GroupWithZero G<VAR>a : G<VAR>ha : a ≠ 0<GOAL>⇑(Equiv.mulRight₀ a ha) = fun x => x * a
<VAR>G : Type u_1<VAR>GroupWithZero G<VAR>a : G<VAR>ha : a ≠ 0<GOAL>⇑(Equiv.symm (Equiv.mulRight₀ a ha)) = fun x => x * a⁻¹
<VAR>G : Type u_1<VAR>GroupWithZero G<VAR>a : G<VAR>ha : a ≠ 0<GOAL>Function.Bijective fun x => x * a
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>LieAlgebra.derivedSeriesOfIdeal R L 0 I = I
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I = ⁅LieAlgebra.derivedSeriesOfIdeal R L k I, LieAlgebra.derivedSeriesOfIdeal R L k I⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>k : ℕ<GOAL>LieAlgebra.derivedSeries R L k = LieAlgebra.derivedSeriesOfIdeal R L k ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k l : ℕ<GOAL>LieAlgebra.derivedSeriesOfIdeal R L (k + l) I = LieAlgebra.derivedSeriesOfIdeal R L k (LieAlgebra.derivedSeriesOfIdeal R L l I)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I J : LieIdeal R L<VAR>k l : ℕ<VAR>h₁ : I ≤ J<VAR>h₂ : l ≤ k<GOAL>LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L l J
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I ≤ LieAlgebra.derivedSeriesOfIdeal R L k I
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>LieAlgebra.derivedSeriesOfIdeal R L k I ≤ I
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I J : LieIdeal R L<VAR>h : I ≤ J<VAR>k : ℕ<GOAL>LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L k J
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k l : ℕ<VAR>h : l ≤ k<GOAL>LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L l I
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I J : LieIdeal R L<VAR>k l : ℕ<GOAL>LieAlgebra.derivedSeriesOfIdeal R L (k + l) (I + J) ≤ LieAlgebra.derivedSeriesOfIdeal R L k I + LieAlgebra.derivedSeriesOfIdeal R L l J
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>k : ℕ<GOAL>LieAlgebra.derivedSeriesOfIdeal R L k ⊥ = ⊥
<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 ↔ LieAlgebra.derivedSeriesOfIdeal R L 1 I = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>IsLieAbelian ↥↑(LieAlgebra.derivedSeriesOfIdeal R L k I) ↔ LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>LieAlgebra.derivedSeries R (↥↑I) k = LieIdeal.comap I.incl (LieAlgebra.derivedSeriesOfIdeal R L k I)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>LieIdeal.map I.incl (LieAlgebra.derivedSeries R (↥↑I) k) = LieAlgebra.derivedSeriesOfIdeal R L k I
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>LieAlgebra.derivedSeries R (↥↑I) k = ⊥ ↔ LieAlgebra.derivedSeriesOfIdeal R L k I = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>k l : ℕ<VAR>I J : LieIdeal R L<VAR>hI : LieAlgebra.derivedSeries R (↥↑I) k = ⊥<VAR>hJ : LieAlgebra.derivedSeries R (↥↑J) l = ⊥<GOAL>LieAlgebra.derivedSeries R (↥↑(I + J)) (k + l) = ⊥
<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>k : ℕ<GOAL>LieIdeal.map f (LieAlgebra.derivedSeries R L' k) ≤ LieAlgebra.derivedSeries R L k
<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>k : ℕ<VAR>h : Function.Surjective ⇑f<GOAL>LieIdeal.map f (LieAlgebra.derivedSeries R L' k) = LieAlgebra.derivedSeries R L k
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>n : ℕ<GOAL>LieAlgebra.derivedSeries R L (n + 1) = ⊤ ↔ LieAlgebra.derivedSeries R L 1 = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>n : ℕ<VAR>h : LieAlgebra.derivedSeries R L 1 = ⊤<GOAL>LieAlgebra.derivedSeries R L n = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>self : LieAlgebra.IsSolvable R L<GOAL>∃ k, LieAlgebra.derivedSeries R L k = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsSolvable R L<VAR>Nontrivial L<GOAL>LieAlgebra.derivedSeries R L 1 < ⊤
<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₁ : LieAlgebra.IsSolvable R L<VAR>h₂ : Function.Injective ⇑f<GOAL>LieAlgebra.IsSolvable R L'
<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₁ : LieAlgebra.IsSolvable R L'<VAR>h₂ : Function.Surjective ⇑f<GOAL>LieAlgebra.IsSolvable R L
<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>LieAlgebra.IsSolvable R L'<GOAL>LieAlgebra.IsSolvable R ↥f.range
<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>e : L' ≃ₗ⁅R⁆ L<GOAL>LieAlgebra.IsSolvable R L' ↔ LieAlgebra.IsSolvable R L
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I J : LieIdeal R L<VAR>h₁ : I ≤ J<GOAL>LieAlgebra.IsSolvable R ↥↑J → LieAlgebra.IsSolvable R ↥↑I
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>IsNoetherian R L<VAR>I : LieIdeal R L<GOAL>LieAlgebra.IsSolvable R ↥↑I ↔ I ≤ LieAlgebra.radical R L
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>LieAlgebra.center R L ≤ LieAlgebra.radical R L
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsSolvable R L<GOAL>LieAlgebra.radical 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>k : ℕ<GOAL>LieAlgebra.derivedLengthOfIdeal R L I = k + 1 ↔ IsLieAbelian ↥↑(LieAlgebra.derivedSeriesOfIdeal R L k I) ∧ LieAlgebra.derivedSeriesOfIdeal R L k I ≠ ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>LieAlgebra.derivedLength R ↥↑I = LieAlgebra.derivedLengthOfIdeal R L I
<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 ↥↑(LieAlgebra.derivedAbelianOfIdeal I)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>hI : LieAlgebra.IsSolvable R ↥↑I<GOAL>LieAlgebra.derivedLengthOfIdeal R L I = 0 ↔ I = ⊥
<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 : LieAlgebra.IsSolvable R ↥↑I<GOAL>LieAlgebra.derivedAbelianOfIdeal I = ⊥ ↔ I = ⊥
<VAR>G₀ : Type u_3<VAR>MulZeroClass G₀<VAR>a : G₀<GOAL>SemiconjBy a 0 0
<VAR>G₀ : Type u_3<VAR>MulZeroClass G₀<VAR>x y : G₀<GOAL>SemiconjBy 0 x y
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a x y : G₀<GOAL>SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a x y : G₀<VAR>h : SemiconjBy a x y<GOAL>SemiconjBy a⁻¹ y x
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a x y : G₀<VAR>h : SemiconjBy a x y<GOAL>SemiconjBy a x⁻¹ y⁻¹
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a x y : G₀<GOAL>SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a x y x' y' : G₀<VAR>h : SemiconjBy a x y<VAR>h' : SemiconjBy a x' y'<GOAL>SemiconjBy a (x / x') (y / y')
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a x y : G₀<VAR>h : SemiconjBy a x y<VAR>m : ℤ<GOAL>SemiconjBy a (x ^ m) (y ^ m)
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>h : Commute a b<VAR>m : ℤ<GOAL>Commute a (b ^ m)
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>h : Commute a b<VAR>m : ℤ<GOAL>Commute (a ^ m) b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>h : Commute a b<VAR>m n : ℤ<GOAL>Commute (a ^ m) (b ^ n)
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>n : ℤ<GOAL>Commute (a ^ n) a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>n : ℤ<GOAL>Commute a (a ^ n)
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>m n : ℤ<GOAL>Commute (a ^ m) (a ^ n)
<VAR>M₀ : Type u_2<VAR>MulZeroClass M₀<VAR>a b : M₀<GOAL>a * b ≠ 0 → a ≠ 0
<VAR>M₀ : Type u_2<VAR>MulZeroClass M₀<VAR>a b : M₀<GOAL>a * b ≠ 0 → b ≠ 0
<VAR>M₀ : Type u_2<VAR>MulZeroClass M₀<VAR>a b : M₀<VAR>h : a * b ≠ 0<GOAL>a ≠ 0 ∧ b ≠ 0
<VAR>M₀ : Type u_2<VAR>MulZeroClass M₀<VAR>a b : M₀<VAR>h : a ≠ 0 → b = 0<GOAL>a * b = 0
<VAR>M₀ : Type u_2<VAR>MulZeroClass M₀<GOAL>(fun x => 0 * x) = Function.const M₀ 0
<VAR>M₀ : Type u_2<VAR>MulZeroClass M₀<GOAL>(fun x => x * 0) = Function.const M₀ 0
<VAR>M₀ : Type u_2<VAR>Mul M₀<VAR>Zero M₀<VAR>NoZeroDivisors M₀<VAR>a : M₀<VAR>h : a * a = 0<GOAL>a = 0
<VAR>M₀ : Type u_2<VAR>Mul M₀<VAR>Zero M₀<VAR>NoZeroDivisors M₀<VAR>a b : M₀<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a * b ≠ 0
<VAR>M₀ : Type u_2<VAR>MulZeroOneClass M₀<VAR>h : 0 = 1<VAR>a : M₀<GOAL>a = 0
<VAR>M₀ : Type u_2<VAR>MulZeroOneClass M₀<GOAL>0 = 1 ↔ Subsingleton M₀
<VAR>M₀ : Type u_2<VAR>MulZeroOneClass M₀<VAR>h : 0 = 1<VAR>a b : M₀<GOAL>a = b
<VAR>M₀ : Type u_2<VAR>MulZeroOneClass M₀<GOAL>0 ≠ 1 ∨ ∀ (a : M₀), a = 0
<VAR>M₀ : Type u_2<VAR>MulZeroOneClass M₀<VAR>Nontrivial M₀<VAR>a b : M₀<VAR>h : a * b = 1<GOAL>a ≠ 0
<VAR>M₀ : Type u_2<VAR>MulZeroOneClass M₀<VAR>Nontrivial M₀<VAR>a b : M₀<VAR>h : a * b = 1<GOAL>b ≠ 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>n : ℕ<GOAL>n ≠ 0 → 0 ^ n = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>n : ℕ<GOAL>0 ^ n = if n = 0 then 1 else 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a : M₀<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>ha : a ^ m = 0<GOAL>a ^ n = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a : M₀<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>ha : a ^ n ≠ 0<GOAL>a ≠ 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>n : ℕ<VAR>Nontrivial M₀<GOAL>0 ^ n = 0 ↔ n ≠ 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a : M₀<VAR>NoZeroDivisors M₀<VAR>n : ℕ<GOAL>a ^ n = 0 → a = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a : M₀<VAR>n : ℕ<VAR>NoZeroDivisors M₀<VAR>hn : n ≠ 0<GOAL>a ^ n = 0 ↔ a = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a : M₀<VAR>n : ℕ<VAR>NoZeroDivisors M₀<VAR>hn : n ≠ 0<GOAL>a ^ n ≠ 0 ↔ a ≠ 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a : M₀<VAR>NoZeroDivisors M₀<VAR>n : ℕ<VAR>h : a ≠ 0<GOAL>a ^ n ≠ 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a : M₀<VAR>NoZeroDivisors M₀<GOAL>a ^ 2 = 0 ↔ a = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a : M₀<VAR>n : ℕ<VAR>NoZeroDivisors M₀<VAR>Nontrivial M₀<GOAL>a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
<VAR>M₀ : Type u_2<VAR>CancelMonoidWithZero M₀<VAR>a b c : M₀<GOAL>a * c = b * c ↔ a = b ∨ c = 0
<VAR>M₀ : Type u_2<VAR>CancelMonoidWithZero M₀<VAR>a b c : M₀<GOAL>a * b = a * c ↔ b = c ∨ a = 0
<VAR>M₀ : Type u_2<VAR>CancelMonoidWithZero M₀<VAR>a b : M₀<GOAL>a * b = a ↔ b = 1 ∨ a = 0
<VAR>M₀ : Type u_2<VAR>CancelMonoidWithZero M₀<VAR>a b : M₀<GOAL>a * b = b ↔ a = 1 ∨ b = 0
<VAR>M₀ : Type u_2<VAR>CancelMonoidWithZero M₀<VAR>a b : M₀<VAR>ha : a ≠ 0<GOAL>a * b = a ↔ b = 1
<VAR>M₀ : Type u_2<VAR>CancelMonoidWithZero M₀<VAR>a b : M₀<VAR>hb : b ≠ 0<GOAL>a * b = b ↔ a = 1
<VAR>M₀ : Type u_2<VAR>CancelMonoidWithZero M₀<VAR>a b : M₀<VAR>ha : a ≠ 0<GOAL>a = a * b ↔ b = 1
<VAR>M₀ : Type u_2<VAR>CancelMonoidWithZero M₀<VAR>a b : M₀<VAR>hb : b ≠ 0<GOAL>b = a * b ↔ a = 1
<VAR>M₀ : Type u_2<VAR>CancelMonoidWithZero M₀<VAR>a b : M₀<VAR>h₁ : b ≠ 1<VAR>h₂ : a * b = a<GOAL>a = 0
<VAR>M₀ : Type u_2<VAR>CancelMonoidWithZero M₀<VAR>a b : M₀<VAR>h₁ : b ≠ 1<VAR>h₂ : b * a = a<GOAL>a = 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>x : G₀<VAR>h : x ≠ 0<GOAL>Function.Injective fun y => x * y
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>x : G₀<VAR>h : x ≠ 0<GOAL>Function.Injective fun y => y * x
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>b : G₀<VAR>h : b ≠ 0<VAR>a : G₀<GOAL>a * b⁻¹ * b = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<VAR>b : G₀<GOAL>a⁻¹ * (a * b) = b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>h : a * b = 1<GOAL>a⁻¹ = b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>0 / a = 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>a / 0 = 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>a * a * a⁻¹ = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>a * a⁻¹ * a = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>a⁻¹ * a * a = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>a * a / a = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>a / a * a = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>a / (a * a) = a⁻¹
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>1 / a ≠ 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>a⁻¹ = 0 ↔ a = 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>0 = a⁻¹ ↔ 0 = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>a / (a / a) = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : 1 / a ≠ 0<GOAL>a ≠ 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : 1 / a = 0<GOAL>a = 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>Function.Surjective fun g => a * g
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>Function.Surjective fun g => g * a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>n : ℤ<GOAL>n ≠ 0 → 0 ^ n = 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>n : ℤ<GOAL>0 ^ n = if n = 0 then 1 else 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>ha : a ≠ 0<VAR>n : ℤ<GOAL>a ^ (n + 1) = a ^ n * a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>ha : a ≠ 0<VAR>n : ℤ<GOAL>a ^ (n - 1) = a ^ n * a⁻¹
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>ha : a ≠ 0<VAR>m n : ℤ<GOAL>a ^ (m + n) = a ^ m * a ^ n
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>m n : ℤ<VAR>h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0<GOAL>a ^ (m + n) = a ^ m * a ^ n
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<VAR>i : ℤ<GOAL>a ^ (1 + i) = a * a ^ i
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a b c : G₀<GOAL>a / c * b = a * b / c
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a b : G₀<GOAL>a ^ 2 * b / a = a * b
<VAR>M : Type u_10<VAR>A : Type u_11<VAR>Zero A<VAR>self : SMulZeroClass M A<VAR>a : M<GOAL>a • 0 = 0
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Zero A<VAR>SMulZeroClass M A<VAR>a : M<GOAL>a • 0 = 0
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Zero A<VAR>SMulZeroClass M A<VAR>p : Prop<VAR>Decidable p<VAR>a : M<VAR>b : A<GOAL>(a • if p then b else 0) = if p then a • b else 0
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Zero A<VAR>SMulZeroClass M A<VAR>a : M<VAR>b : A<VAR>h : b = 0<GOAL>a • b = 0
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Zero A<VAR>SMulZeroClass M A<VAR>a : M<VAR>b : A<GOAL>a • b ≠ 0 → b ≠ 0
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Zero A<VAR>SMulZeroClass M A<VAR>x : M<GOAL>∀ (x_1 : A), (SMulZeroClass.toZeroHom A x) x_1 = x • x_1
<VAR>M : Type u_10<VAR>A : Type u_11<VAR>AddZeroClass A<VAR>self : DistribSMul M A<VAR>a : M<VAR>x y : A<GOAL>a • (x + y) = a • x + a • y
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>AddZeroClass A<VAR>DistribSMul M A<VAR>a : M<VAR>b₁ b₂ : A<GOAL>a • (b₁ + b₂) = a • b₁ + a • b₂
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>AddZeroClass A<VAR>DistribSMul M A<VAR>x : M<GOAL>∀ (x_1 : A), (DistribSMul.toAddMonoidHom A x) x_1 = (fun x x_2 => x • x_2) x x_1
<VAR>M : Type u_10<VAR>A : Type u_11<VAR>Monoid M<VAR>AddMonoid A<VAR>self : DistribMulAction M A<VAR>a : M<GOAL>a • 0 = 0
<VAR>M : Type u_10<VAR>A : Type u_11<VAR>Monoid M<VAR>AddMonoid A<VAR>self : DistribMulAction M A<VAR>a : M<VAR>x y : A<GOAL>a • (x + y) = a • x + a • y
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Monoid M<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>x : M<GOAL>∀ (x_1 : A), (DistribMulAction.toAddMonoidHom A x) x_1 = x • x_1
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Monoid M<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>x : M<GOAL>(DistribMulAction.toAddMonoidEnd M A) x = DistribMulAction.toAddMonoidHom A x
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Monoid M<VAR>AddGroup A<VAR>DistribMulAction M A<VAR>r : M<VAR>x : A<GOAL>r • -x = -(r • x)
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Monoid M<VAR>AddGroup A<VAR>DistribMulAction M A<VAR>r : M<VAR>x y : A<GOAL>r • (x - y) = r • x - r • y
<VAR>M : Type u_10<VAR>A : Type u_11<VAR>Monoid M<VAR>Monoid A<VAR>self : MulDistribMulAction M A<VAR>r : M<VAR>x y : A<GOAL>r • (x * y) = r • x * r • y