ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_10<VAR>A : Type u_11<VAR>Monoid M<VAR>Monoid A<VAR>self : MulDistribMulAction M A<VAR>r : M<GOAL>r • 1 = 1
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Monoid M<VAR>Monoid A<VAR>MulDistribMulAction 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>Monoid M<VAR>Monoid A<VAR>MulDistribMulAction M A<VAR>r : M<VAR>x : A<GOAL>(MulDistribMulAction.toMonoidHom A r) x = r • x
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Monoid M<VAR>Monoid A<VAR>MulDistribMulAction M A<VAR>r : M<VAR>x : A<VAR>n : ℕ<GOAL>r • x ^ n = (r • x) ^ n
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Monoid M<VAR>Monoid A<VAR>MulDistribMulAction M A<VAR>r : M<GOAL>(MulDistribMulAction.toMonoidEnd M A) r = MulDistribMulAction.toMonoidHom A r
<VAR>M : Type u_1<VAR>A : Type u_4<VAR>Monoid M<VAR>Group A<VAR>MulDistribMulAction 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>Group A<VAR>MulDistribMulAction M A<VAR>r : M<VAR>x y : A<GOAL>r • (x / y) = r • x / r • y
<VAR>α : Type u_6<VAR>AddMonoid α<VAR>f : AddMonoid.End α<VAR>a : α<GOAL>f • a = f a
<VAR>I : Type u<VAR>f : I → Type v<VAR>α : Type u_1<VAR>Monoid α<VAR>(i : I) → AddMonoid (f i)<VAR>(i : I) → DistribMulAction α (f i)<VAR>DecidableEq I<VAR>i : I<VAR>r : α<VAR>x : f i<GOAL>Pi.single i (r • x) = r • Pi.single i x
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>AddMonoid β<VAR>DistribMulAction α β<VAR>DecidableEq I<VAR>i : I<VAR>r : α<VAR>x : β<GOAL>Pi.single i (r • x) = r • Pi.single i x
<VAR>I : Type u<VAR>f : I → Type v<VAR>g : I → Type u_1<VAR>(i : I) → MonoidWithZero (f i)<VAR>(i : I) → AddMonoid (g i)<VAR>(i : I) → DistribMulAction (f i) (g i)<VAR>DecidableEq I<VAR>i : I<VAR>r : f i<VAR>x : g i<GOAL>Pi.single i (r • x) = Pi.single i r • Pi.single i x
<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>LieAlgebra.IsNilpotent R L<VAR>self : LieModule.LinearWeights R L M<VAR>χ : L → R<GOAL>LieModule.weightSpace M χ ≠ ⊥ → ∀ (x y : L), χ ⁅x, y⁆ = 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>LieAlgebra.IsNilpotent R L<VAR>self : LieModule.LinearWeights R L M<VAR>χ : L → R<GOAL>LieModule.weightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
<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>LieAlgebra.IsNilpotent R L<VAR>self : LieModule.LinearWeights R L M<VAR>χ : L → R<GOAL>LieModule.weightSpace M χ ≠ ⊥ → ∀ (t : R) (x : L), χ (t • x) = t • χ x
<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>LieAlgebra.IsNilpotent R L<VAR>LieModule.LinearWeights R L M<VAR>χ : LieModule.Weight R L M<VAR>a : L<GOAL>(LieModule.Weight.toLinear R L M χ) a = χ a
<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>LieAlgebra.IsNilpotent R L<VAR>LieModule.LinearWeights R L M<VAR>χ : LieModule.Weight R L M<VAR>x y : L<GOAL>χ ⁅x, y⁆ = 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>LieAlgebra.IsNilpotent R L<VAR>LieModule.LinearWeights R L M<VAR>χ : LieModule.Weight R L M<GOAL>⇑(LieModule.Weight.toLinear R L 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>LieAlgebra.IsNilpotent R L<VAR>LieModule.LinearWeights R L M<VAR>χ : LieModule.Weight R L M<GOAL>LieModule.Weight.toLinear R L M χ = 0 ↔ χ.IsZero
<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>LieAlgebra.IsNilpotent R L<VAR>LieModule.LinearWeights R L M<VAR>χ : LieModule.Weight R L M<GOAL>LieModule.Weight.toLinear R L M χ ≠ 0 ↔ χ.IsNonZero
<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>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>LieAlgebra.IsNilpotent R L<VAR>χ : L → R<GOAL>⇑(LinearMap.trace R ↥↑(LieModule.weightSpace M χ) ∘ₗ ↑(LieModule.toEnd R L ↥↑(LieModule.weightSpace M χ))) = FiniteDimensional.finrank R ↥↑(LieModule.weightSpace 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>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>LieAlgebra.IsNilpotent R L<VAR>χ : L → R<VAR>hχ : LieModule.weightSpace M χ ≠ ⊥<GOAL>0 < FiniteDimensional.finrank R ↥↑(LieModule.weightSpace 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>LieAlgebra.IsNilpotent R L<VAR>χ : L → R<VAR>h : Nontrivial ↥↑(LieModule.shiftedWeightSpace R L M χ)<GOAL>LieModule.weightSpace 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>LieAlgebra.IsNilpotent R L<VAR>LieModule.LinearWeights R L M<VAR>χ : L → R<VAR>x : L<VAR>m : ↥(LieModule.shiftedWeightSpace R L M χ)<GOAL>↑⁅x, m⁆ = ⁅x, ↑m⁆ - χ x • ↑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>LieAlgebra.IsNilpotent R L<VAR>χ : L → R<VAR>a : ↥↑(LieModule.weightSpace M χ)<GOAL>(LieModule.shiftedWeightSpace.shift R L M χ) a = a
<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>LieAlgebra.IsNilpotent R L<VAR>χ : L → R<GOAL>∀ (a : ↥↑(LieModule.weightSpace M χ)), (LieModule.shiftedWeightSpace.shift R L M χ).symm a = a
<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>LieAlgebra.IsNilpotent R L<VAR>LieModule.LinearWeights R L M<VAR>χ : L → R<VAR>x : L<GOAL>(LieModule.toEnd R L ↥↑(LieModule.shiftedWeightSpace R L M χ)) x = (LieModule.shiftedWeightSpace.shift R L M χ).conj ((LieModule.toEnd R L ↥↑(LieModule.weightSpace M χ)) x - χ x • LinearMap.id)
<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>LieAlgebra.IsNilpotent R L<VAR>LieModule.LinearWeights R L M<VAR>IsNoetherian R M<VAR>χ : LieModule.Weight R L M<GOAL>∃ m, m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = χ x • m
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>Nontrivial M₀<VAR>u : M₀ˣ<GOAL>↑u ≠ 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>u : M₀ˣ<VAR>a : M₀<GOAL>a * ↑u = 0 ↔ a = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>u : M₀ˣ<VAR>a : M₀<GOAL>↑u * a = 0 ↔ a = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>Nontrivial M₀<VAR>a : M₀<VAR>ha : IsUnit a<GOAL>a ≠ 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a b : M₀<VAR>ha : IsUnit a<GOAL>a * b = 0 ↔ b = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a b : M₀<VAR>hb : IsUnit b<GOAL>a * b = 0 ↔ a = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<GOAL>IsUnit 0 ↔ 0 = 1
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>Nontrivial M₀<GOAL>¬IsUnit 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>u : M₀ˣ<GOAL>Ring.inverse ↑u = ↑u⁻¹
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>x : M₀<VAR>h : ¬IsUnit x<GOAL>Ring.inverse x = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>x : M₀<VAR>h : IsUnit x<GOAL>x * Ring.inverse x = 1
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>x : M₀<VAR>h : IsUnit x<GOAL>Ring.inverse x * x = 1
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>x y : M₀<VAR>h : IsUnit x<GOAL>y * x * Ring.inverse x = y
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>x y : M₀<VAR>h : IsUnit x<GOAL>y * Ring.inverse x * x = y
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>x y : M₀<VAR>h : IsUnit x<GOAL>x * (Ring.inverse x * y) = y
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>x y : M₀<VAR>h : IsUnit x<GOAL>Ring.inverse x * (x * y) = y
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>x y z : M₀<VAR>h : IsUnit x<GOAL>Ring.inverse x * y = z ↔ y = x * z
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>x y z : M₀<VAR>h : IsUnit z<GOAL>x = y * Ring.inverse z ↔ x * z = y
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<GOAL>Ring.inverse 1 = 1
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<GOAL>Ring.inverse 0 = 0
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a : M₀<GOAL>IsUnit a → IsUnit (Ring.inverse a)
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a : M₀<GOAL>IsUnit (Ring.inverse a) ↔ IsUnit a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>h : 1 ≠ 0 := ⋯<GOAL>Units.mk0 1 h = 1
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>↑(Units.mk0 a h) = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>u : G₀ˣ<VAR>h : ↑u ≠ 0<GOAL>Units.mk0 (↑u) h = u
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>u : G₀ˣ<GOAL>↑u * (↑u)⁻¹ = 1
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>u : G₀ˣ<GOAL>(↑u)⁻¹ * ↑u = 1
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>Units.mk0 a ha = Units.mk0 b hb ↔ a = b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>p : G₀ˣ → Prop<GOAL>(∃ g, p g) ↔ ∃ g hg, p (Units.mk0 g hg)
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>p : (g : G₀) → g ≠ 0 → Prop<GOAL>(∃ g hg, p g hg) ↔ ∃ g, p ↑g ⋯
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>p : G₀ → Prop<GOAL>(∃ u, p ↑u) ↔ ∃ x, x ≠ 0 ∧ p x
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>a = 0 ∨ ∃ u, a = ↑u
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>x : G₀<VAR>hx : x ≠ 0<GOAL>IsUnit x
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>IsUnit a ↔ a ≠ 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>x y : G₀<VAR>hxy : x * y ≠ 0<GOAL>Units.mk0 (x * y) hxy = Units.mk0 x ⋯ * Units.mk0 y ⋯
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a / b ≠ 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<GOAL>a / b = 0 ↔ a = 0 ∨ b = 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<GOAL>a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>a / a = 1
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hc : c ≠ 0<GOAL>a = b * c⁻¹ ↔ a * c = b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hb : b ≠ 0<GOAL>a = b⁻¹ * c ↔ b * a = c
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>ha : a ≠ 0<GOAL>a⁻¹ * b = c ↔ b = a * c
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hb : b ≠ 0<GOAL>a * b⁻¹ = c ↔ a = c * b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>hb : b ≠ 0<GOAL>a * b⁻¹ = 1 ↔ a = b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>ha : a ≠ 0<GOAL>a⁻¹ * b = 1 ↔ a = b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>hb : b ≠ 0<GOAL>a * b = 1 ↔ a = b⁻¹
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>ha : a ≠ 0<GOAL>a * b = 1 ↔ a⁻¹ = b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>ha : a ≠ 0<VAR>h : a = c * b⁻¹<GOAL>a * b = c
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hb : b ≠ 0<VAR>h : b = a⁻¹ * c<GOAL>a * b = c
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hc : c ≠ 0<VAR>h : b⁻¹ * a = c<GOAL>a = b * c
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hb : b ≠ 0<VAR>h : a * c⁻¹ = b<GOAL>a = b * c
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>b : G₀<VAR>a : G₀<VAR>h : b ≠ 0<GOAL>a / b * b = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>a * (1 / a) = 1
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>1 / a * a = 1
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hc : c ≠ 0<GOAL>a / c = b / c ↔ a = b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hb : b ≠ 0<GOAL>a / b = c ↔ a = c * b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hb : b ≠ 0<GOAL>c = a / b ↔ c * b = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hb : b ≠ 0<GOAL>a / b = c ↔ c * b = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hc : c ≠ 0<GOAL>a = b / c ↔ a * c = b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hb : b ≠ 0<GOAL>a = c * b → a / b = c
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hc : c ≠ 0<GOAL>a * c = b → a = b / c
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>hb : b ≠ 0<GOAL>a / b = 1 ↔ a = b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>b : G₀<VAR>hb : b ≠ 0<VAR>a : G₀<GOAL>b / (a * b) = a⁻¹
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>hb : b ≠ 0<GOAL>b / (a * b) = 1 / a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>c : G₀<VAR>a b : G₀<VAR>hc : c ≠ 0<GOAL>a * c / (b * c) = a / b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>b : G₀<VAR>a : G₀<VAR>hb : b ≠ 0<GOAL>a = a * b * (1 / b)
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>b c : G₀<VAR>a : G₀<VAR>hc : c ≠ 0<GOAL>a / c / (b / c) = a / b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>b c : G₀<VAR>a : G₀<VAR>hc : c ≠ 0<GOAL>a / c * (c / b) = a / b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>h : b = 0 → a = 0<GOAL>a / b * b = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>h : b = 0 → a = 0<GOAL>a * b / b = a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>b : G₀<VAR>a : G₀<VAR>hb : b ≠ 0<GOAL>a /ₚ Units.mk0 b hb = a / b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>ha : a ≠ 0<VAR>h : n ≤ m<GOAL>a ^ (m - n) = a ^ m * (a ^ n)⁻¹
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>h : n < m<GOAL>a ^ (m - n) = a ^ m * (a ^ n)⁻¹
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>m n : ℕ<VAR>ha : a ≠ 0<VAR>h : n ≤ m<GOAL>a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>h : n < m<GOAL>a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
<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>n : ℤ<GOAL>a ≠ 0 → a ^ n ≠ 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>n : ℤ<GOAL>a ^ n = 0 → a = 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>a ^ n = 0 ↔ a = 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>a ^ n ≠ 0 ↔ a ≠ 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>n : ℤ<VAR>ha : a ≠ 0<GOAL>a ^ (-n) * a ^ n = 1
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<GOAL>Ring.inverse a = a⁻¹
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<GOAL>Ring.inverse = Inv.inv
<VAR>α : Type u_1<VAR>GroupWithZero α<VAR>a : { a // a ≠ 0 }<GOAL>unitsEquivNeZero.symm a = Units.mk0 ↑a ⋯
<VAR>α : Type u_1<VAR>GroupWithZero α<VAR>a : αˣ<GOAL>↑(unitsEquivNeZero a) = ↑a
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a : G₀<VAR>ha : a ≠ 0<VAR>b : G₀<GOAL>a / (a * b) = b⁻¹
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a : G₀<VAR>b : G₀<VAR>ha : a ≠ 0<GOAL>a / (a * b) = 1 / b
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a b : G₀<VAR>h : a = 0 → b = 0<GOAL>a * b / a = b
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a b : G₀<VAR>h : b = 0 → a = 0<GOAL>b * (a / b) = a
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>b : G₀<VAR>a : G₀<VAR>hb : b ≠ 0<GOAL>b * (a / b) = a
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>c : G₀<VAR>a b : G₀<VAR>hc : c ≠ 0<GOAL>c * a / (c * b) = a / b
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>b d : G₀<VAR>a c : G₀<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<VAR>h : a / b = c / d<GOAL>a * d = c * b
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a b c d : G₀<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<GOAL>a / b = c / d ↔ a * d = c * b
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a b c d : G₀<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<GOAL>a / b = c / d ↔ a / c = b / d
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a b : G₀<VAR>ha : a ≠ 0<GOAL>a / (a / b) = b
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a b : G₀<VAR>ha : a ≠ 0<GOAL>a / b / a = b⁻¹
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>a : G₀<VAR>b : G₀<VAR>h : a ≠ 0<GOAL>1 / (a * b) * a = 1 / b
<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>c : G₀<VAR>a b : G₀<VAR>hc : c ≠ 0<GOAL>c / a / (c / b) = b / a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<GOAL>(IsCauSeq abs fun n => ∑ i ∈ Finset.range n, a i) → IsCauSeq abv fun n => ∑ i ∈ Finset.range n, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>hf : IsCauSeq abs fun m => ∑ n ∈ Finset.range m, abv (f n)<GOAL>IsCauSeq abv fun m => ∑ n ∈ Finset.range m, f n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>ha : IsCauSeq abs fun m => ∑ n ∈ Finset.range m, abv (f n)<VAR>hb : IsCauSeq abv fun m => ∑ n ∈ Finset.range m, g n<VAR>ε : α<VAR>ε0 : 0 < ε<GOAL>∃ i, ∀ j ≥ i, abv ((∑ k ∈ Finset.range j, f k) * ∑ k ∈ Finset.range j, g k - ∑ n ∈ Finset.range j, ∑ m ∈ Finset.range (n + 1), f m * g (n - m)) < ε
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>f : ℕ → α<VAR>a : α<VAR>m : ℕ<VAR>ham : ∀ n ≥ m, |f n| ≤ a<VAR>hnm : ∀ n ≥ m, f n.succ ≤ f n<GOAL>IsCauSeq abs f
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>f : ℕ → α<VAR>a : α<VAR>m : ℕ<VAR>ham : ∀ n ≥ m, |f n| ≤ a<VAR>hnm : ∀ n ≥ m, f n ≤ f n.succ<GOAL>IsCauSeq abs f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>Archimedean α<VAR>Nontrivial β<VAR>x : β<VAR>hx1 : abv x < 1<GOAL>IsCauSeq abv fun n => ∑ m ∈ Finset.range n, x ^ m
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>a : α<VAR>x : α<VAR>hx1 : |x| < 1<GOAL>IsCauSeq abs fun m => ∑ n ∈ Finset.range m, a * x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>Archimedean α<VAR>f : ℕ → β<VAR>n : ℕ<VAR>r : α<VAR>hr0 : 0 ≤ r<VAR>hr1 : r < 1<VAR>h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)<GOAL>IsCauSeq abv fun m => ∑ n ∈ Finset.range m, f 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>N : LieSubmodule R L M<VAR>I : LieIdeal R L<GOAL>⁅I, N⁆ = LieSubmodule.lieSpan R L {m | ∃ x n, ⁅↑x, ↑n⁆ = 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>I : LieIdeal R L<GOAL>↑⁅I, N⁆ = Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = 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>I : LieIdeal R L<GOAL>↑⁅I, N⁆ = Submodule.span R {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = 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>N N' : LieSubmodule R L M<VAR>I : LieIdeal R L<GOAL>⁅I, N⁆ ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, 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>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>x : ↥I<VAR>m : ↥N<GOAL>⁅↑x, ↑m⁆ ∈ ⁅I, 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>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>m : M<VAR>hx : x ∈ I<VAR>hm : m ∈ N<GOAL>⁅x, m⁆ ∈ ⁅I, N⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I J : LieIdeal R L<GOAL>⁅I, J⁆ = ⁅J, 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<GOAL>⁅I, N⁆ ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I J : LieIdeal R L<GOAL>⁅I, J⁆ ≤ 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<GOAL>⁅I, J⁆ ≤ I ⊓ J
<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>I : LieIdeal R L<GOAL>⁅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<GOAL>⁅⊥, 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>N : LieSubmodule R L M<VAR>I : LieIdeal R L<GOAL>⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>h₁ : I ≤ J<VAR>h₂ : N ≤ N'<GOAL>⁅I, N⁆ ≤ ⁅J, 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>N : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>h : I ≤ J<GOAL>⁅I, N⁆ ≤ ⁅J, 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>N N' : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : N ≤ N'<GOAL>⁅I, N⁆ ≤ ⁅I, 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>N N' : LieSubmodule R L M<VAR>I : LieIdeal R L<GOAL>⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, 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>N : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, 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>N N' : LieSubmodule R L M<VAR>I : LieIdeal R L<GOAL>⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ⊓ ⁅I, 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>N : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ⊓ ⁅J, N⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>LieSubmodule.map f ⁅I, N⁆ = ⁅I, LieSubmodule.map f N⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>LieSubmodule.map f (LieSubmodule.comap f N₂) ≤ N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : N₂ ≤ f.range<GOAL>LieSubmodule.map f (LieSubmodule.comap f N₂) = N₂