ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>ι : Sort u_1<VAR>S : ι → Subalgebra R A<VAR>x : A<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>ι : Sort u_1<VAR>S : ι → Subalgebra R A<GOAL>Subalgebra.toSubmodule (⨅ i, S i) = ⨅ i, Subalgebra.toSubmodule (S i)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap R A)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Subalgebra.toSubmodule ⊥ = 1
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>↑⊥ = Set.range ⇑(algebraMap R A)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S = ⊤ ↔ ∀ (x : A), x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>f.range = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>(AlgHom.id R A).range = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>Subalgebra.map f ⊤ = f.range
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>Subalgebra.map f ⊥ = ⊥
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>Subalgebra.comap f ⊤ = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Function.Surjective ⇑(algebraMap R A) ↔ ⊤ = ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Field R<VAR>Semiring A<VAR>Nontrivial A<VAR>Algebra R A<GOAL>Function.Bijective ⇑(algebraMap R A) ↔ ⊤ = ⊥
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>Field F<VAR>Semiring R<VAR>Nontrivial R<VAR>Algebra F R<GOAL>∀ (a : F), (Algebra.botEquiv F R).symm a = (Algebra.ofId F ↥⊥) a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<GOAL>↑(Subalgebra.topEquiv.symm a) = a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : ↥⊤<GOAL>Subalgebra.topEquiv a = ↑a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.val.range = S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<VAR>h : S ≤ T<GOAL>Function.Injective ⇑(Subalgebra.inclusion h)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>Subalgebra.inclusion ⋯ = AlgHom.id R ↥S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<VAR>h : S ≤ T<VAR>x : A<VAR>hx : x ∈ S<GOAL>(Subalgebra.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<VAR>h : S ≤ T<VAR>x : ↥T<VAR>m : ↑x ∈ S<GOAL>(Subalgebra.inclusion h) ⟨↑x, m⟩ = x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T U : Subalgebra R A<VAR>hst : S ≤ T<VAR>htu : T ≤ U<VAR>x : ↥S<GOAL>(Subalgebra.inclusion htu) ((Subalgebra.inclusion hst) x) = (Subalgebra.inclusion ⋯) x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<VAR>h : S ≤ T<VAR>s : ↥S<GOAL>↑((Subalgebra.inclusion h) s) = ↑s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<VAR>h : S = T<VAR>x : ↥S<GOAL>(S.equivOfEq T h) x = ⟨↑x, ⋯⟩
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<VAR>h : S = T<GOAL>(S.equivOfEq T h).symm = T.equivOfEq S ⋯
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.equivOfEq S ⋯ = AlgEquiv.refl
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T U : Subalgebra R A<VAR>hST : S = T<VAR>hTU : T = U<GOAL>(S.equivOfEq T hST).trans (T.equivOfEq U hTU) = S.equivOfEq U ⋯
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>S : Subalgebra R A<VAR>f : A →ₐ[R] B<GOAL>(f.comp S.val).range = Subalgebra.map f S
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>S : Subalgebra R A<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>x : ↥S<GOAL>↑((S.equivMapOfInjective f hf) x) = f ↑x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>α : Type u_1<VAR>SMul A α<VAR>S : Subalgebra R A<VAR>g : ↥S<VAR>m : α<GOAL>g • m = ↑g • m
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Semiring α<VAR>Algebra R A<VAR>Algebra A α<VAR>S : Subalgebra R A<GOAL>algebraMap (↥S) α = (algebraMap A α).comp ↑S.val
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>(algebraMap (↥S) A).rangeS = S.toSubsemiring
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>(algebraMap (↥S) A).range = S.toSubring
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(algebraMap R A) r ∈ Set.center A
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>↑(Subalgebra.center R A) = Set.center A
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>(Subalgebra.center R A).toSubsemiring = Subsemiring.center A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<GOAL>(Subalgebra.center R A).toSubring = Subring.center A
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u_1<VAR>CommSemiring A<VAR>Algebra R A<GOAL>Subalgebra.center R A = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<GOAL>a ∈ Subalgebra.center R A ↔ ∀ (b : A), b * a = a * b
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>r : R<GOAL>(algebraMap R A) r ∈ s.centralizer
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>↑(Subalgebra.centralizer R s) = s.centralizer
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>z : A<GOAL>z ∈ Subalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>Subalgebra.center R A ≤ Subalgebra.centralizer R s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s t : Set A<VAR>h : s ⊆ t<GOAL>Subalgebra.centralizer R t ≤ Subalgebra.centralizer R s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>Subalgebra.centralizer R s = ⊤ ↔ s ⊆ ↑(Subalgebra.center R A)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Subalgebra.centralizer R Set.univ = Subalgebra.center R A
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Subalgebra R A<GOAL>s ≤ Subalgebra.centralizer R ↑(Subalgebra.centralizer R ↑s)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>Subalgebra.centralizer R s.centralizer.centralizer = Subalgebra.centralizer R s
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : R<VAR>S : Subsemiring R<GOAL>x ∈ subalgebraOfSubsemiring S ↔ x ∈ S
<VAR>R : Type u_1<VAR>Ring R<VAR>x : R<VAR>S : Subring R<GOAL>x ∈ subalgebraOfSubring S ↔ x ∈ S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>F : Type u_4<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>φ ψ : F<VAR>x : A<GOAL>x ∈ AlgHom.equalizer φ ψ ↔ φ x = ψ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>F : Type u_4<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>φ ψ : F<GOAL>Subalgebra.toSubmodule (AlgHom.equalizer φ ψ) = LinearMap.eqLocus φ ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>F : Type u_4<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>φ ψ : F<GOAL>AlgHom.equalizer φ ψ = ⊤ ↔ φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>F : Type u_4<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>φ : F<GOAL>AlgHom.equalizer φ φ = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>F : Type u_4<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>φ ψ : F<VAR>S : Subalgebra R A<GOAL>S ≤ AlgHom.equalizer φ ψ ↔ Set.EqOn ⇑φ ⇑ψ ↑S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>F : Type u_4<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>φ ψ : F<VAR>S T : Subalgebra R A<VAR>hS : Set.EqOn ⇑φ ⇑ψ ↑S<VAR>hT : Set.EqOn ⇑φ ⇑ψ ↑T<GOAL>Set.EqOn ⇑φ ⇑ψ ↑(S ⊔ T)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>F : Type u_4<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>φ ψ : F<VAR>S T : Subalgebra R A<VAR>hST : Codisjoint S T<VAR>hS : Set.EqOn ⇑φ ⇑ψ ↑S<VAR>hT : Set.EqOn ⇑φ ⇑ψ ↑T<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>S : Subalgebra R B<GOAL>Subalgebra.map f (Subalgebra.comap f S) = S ⊓ f.range
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>S : Subalgebra R B<VAR>h : S ≤ f.range<GOAL>Subalgebra.map f (Subalgebra.comap f S) = S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Surjective ⇑f<VAR>S : Subalgebra R B<GOAL>Subalgebra.map f (Subalgebra.comap f S) = S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>S : Subalgebra R A<GOAL>Subalgebra.comap f (Subalgebra.map f S) = S
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>(i : I) → NonUnitalNonAssocSemiring (f i)<VAR>NonUnitalNonAssocSemiring γ<VAR>g : (i : I) → γ →ₙ+* f i<VAR>x : γ<VAR>b : I<GOAL>(Pi.nonUnitalRingHom g) x b = (g b) x
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>Nonempty I<VAR>(i : I) → NonUnitalNonAssocSemiring (f i)<VAR>NonUnitalNonAssocSemiring γ<VAR>g : (i : I) → γ →ₙ+* f i<VAR>hg : ∀ (i : I), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(Pi.nonUnitalRingHom g)
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>(i : I) → NonAssocSemiring (f i)<VAR>NonAssocSemiring γ<VAR>g : (i : I) → γ →+* f i<VAR>x : γ<VAR>b : I<GOAL>(Pi.ringHom g) x b = (g b) x
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>Nonempty I<VAR>(i : I) → NonAssocSemiring (f i)<VAR>NonAssocSemiring γ<VAR>g : (i : I) → γ →+* f i<VAR>hg : ∀ (i : I), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(Pi.ringHom g)
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → NonUnitalNonAssocSemiring (f i)<VAR>i : I<VAR>g : (i : I) → f i<GOAL>(Pi.evalNonUnitalRingHom f i) g = g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NonUnitalNonAssocSemiring β<VAR>a : β<GOAL>∀ (a_1 : α), (Pi.constNonUnitalRingHom α β) a a_1 = Function.const α a a_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α →ₙ+* β<VAR>I : Type u_3<VAR>h : I → α<GOAL>∀ (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → NonAssocSemiring (f i)<VAR>i : I<VAR>g : (i : I) → f i<GOAL>(Pi.evalRingHom f i) g = g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NonAssocSemiring β<VAR>a : β<GOAL>∀ (a_1 : α), (Pi.constRingHom α β) a a_1 = Function.const α a a_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NonAssocSemiring α<VAR>NonAssocSemiring β<VAR>f : α →+* β<VAR>I : Type u_3<VAR>h : I → α<GOAL>∀ (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
<VAR>n : ℤ<GOAL>n.negOnePow = (-1) ^ n
<VAR>n₁ n₂ : ℤ<GOAL>(n₁ + n₂).negOnePow = n₁.negOnePow * n₂.negOnePow
<VAR>n : ℤ<VAR>hn : Even n<GOAL>n.negOnePow = 1
<VAR>n : ℤ<GOAL>(2 * n).negOnePow = 1
<VAR>n : ℤ<VAR>hn : Odd n<GOAL>n.negOnePow = -1
<VAR>n : ℤ<GOAL>(2 * n + 1).negOnePow = -1
<VAR>n : ℤ<GOAL>n.negOnePow = 1 ↔ Even n
<VAR>n : ℤ<GOAL>n.negOnePow = -1 ↔ Odd n
<VAR>n : ℤ<GOAL>(-n).negOnePow = n.negOnePow
<VAR>n₁ n₂ : ℤ<GOAL>n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
<VAR>K : Type u_1<VAR>n : ℤ<VAR>Field K<GOAL>↑↑n.negOnePow = (-1) ^ n
<VAR>M : Type u_1<VAR>NonAssocSemiring M<VAR>n : ℕ<GOAL>↑n ∈ Set.center M
<VAR>M : Type u_1<VAR>NonAssocSemiring M<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n ∈ Set.center M
<VAR>M : Type u_1<VAR>NonAssocRing M<VAR>n : ℤ<GOAL>↑n ∈ Set.center M
<VAR>M : Type u_1<VAR>Distrib M<VAR>a b : M<VAR>ha : a ∈ Set.center M<VAR>hb : b ∈ Set.center M<GOAL>a + b ∈ Set.center M
<VAR>M : Type u_1<VAR>NonUnitalNonAssocRing M<VAR>a : M<VAR>ha : a ∈ Set.center M<GOAL>-a ∈ Set.center M
<VAR>R : Type u_1<VAR>self : Distrib R<VAR>a b c : R<GOAL>(a + b) * c = a * c + b * c
<VAR>R : Type u_1<VAR>self : Distrib R<VAR>a b c : R<GOAL>a * (b + c) = a * b + a * c
<VAR>R : Type u_1<VAR>Mul R<VAR>Add R<VAR>self : LeftDistribClass R<VAR>a b c : R<GOAL>a * (b + c) = a * b + a * c
<VAR>R : Type u_1<VAR>Mul R<VAR>Add R<VAR>self : RightDistribClass R<VAR>a b c : R<GOAL>(a + b) * c = a * c + b * c
<VAR>R : Type x<VAR>Mul R<VAR>Add R<VAR>LeftDistribClass R<VAR>a b c : R<GOAL>a * (b + c) = a * b + a * c
<VAR>R : Type x<VAR>Mul R<VAR>Add R<VAR>RightDistribClass R<VAR>a b c : R<GOAL>(a + b) * c = a * c + b * c
<VAR>R : Type x<VAR>Mul R<VAR>Add R<VAR>RightDistribClass R<VAR>a b c d : R<GOAL>(a + b + c) * d = a * d + b * d + c * d
<VAR>α : Type u<VAR>Add α<VAR>MulOneClass α<VAR>RightDistribClass α<VAR>a b : α<GOAL>(a + 1) * b = a * b + b
<VAR>α : Type u<VAR>Add α<VAR>MulOneClass α<VAR>LeftDistribClass α<VAR>a b : α<GOAL>a * (b + 1) = a * b + a
<VAR>α : Type u<VAR>Add α<VAR>MulOneClass α<VAR>RightDistribClass α<VAR>a b : α<GOAL>(1 + a) * b = b + a * b
<VAR>α : Type u<VAR>Add α<VAR>MulOneClass α<VAR>LeftDistribClass α<VAR>a b : α<GOAL>a * (1 + b) = a + a * b
<VAR>α : Type u<VAR>NonAssocSemiring α<VAR>n : α<GOAL>2 * n = n + n
<VAR>α : Type u<VAR>NonAssocSemiring α<VAR>n : α<GOAL>n * 2 = n + n
<VAR>α : Type u_1<VAR>Mul α<VAR>P : Prop<VAR>Decidable P<VAR>a b c : α<GOAL>(a * if P then b else c) = if P then a * b else a * c
<VAR>α : Type u_1<VAR>Add α<VAR>P : Prop<VAR>Decidable P<VAR>a b c : α<GOAL>(a + if P then b else c) = if P then a + b else a + c
<VAR>α : Type u_1<VAR>Add α<VAR>P : Prop<VAR>Decidable P<VAR>a b c : α<GOAL>(if P then a else b) + c = if P then a + c else b + c
<VAR>α : Type u_1<VAR>Mul α<VAR>P : Prop<VAR>Decidable P<VAR>a b c : α<GOAL>(if P then a else b) * c = if P then a * c else b * c
<VAR>α : Type u_1<VAR>Sub α<VAR>P : Prop<VAR>Decidable P<VAR>a b c d : α<GOAL>((if P then a else b) - if P then c else d) = if P then a - c else b - d
<VAR>α : Type u_1<VAR>Add α<VAR>P : Prop<VAR>Decidable P<VAR>a b c d : α<GOAL>((if P then a else b) + if P then c else d) = if P then a + c else b + d
<VAR>α : Type u<VAR>MulZeroClass α<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<GOAL>(if P then a else 0) * b = if P then a * b else 0
<VAR>α : Type u<VAR>MulZeroClass α<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<GOAL>(a * if P then b else 0) = if P then a * b else 0
<VAR>α : Type u<VAR>MulZeroClass α<VAR>P Q : Prop<VAR>Decidable P<VAR>Decidable Q<VAR>a b : α<GOAL>((if P then a else 0) * if Q then b else 0) = if P ∧ Q then a * b else 0
<VAR>α : Type u_1<VAR>MulZeroOneClass α<VAR>P : Prop<VAR>Decidable P<VAR>a : α<GOAL>(a * if P then 1 else 0) = if P then a else 0
<VAR>α : Type u_1<VAR>MulZeroOneClass α<VAR>P : Prop<VAR>Decidable P<VAR>a : α<GOAL>(if P then 1 else 0) * a = if P then a else 0
<VAR>α : Type u<VAR>CommSemiring α<VAR>a b : α<GOAL>(a + b) * (a + b) = a * a + 2 * a * b + b * b
<VAR>α : Type u<VAR>CommSemiring α<VAR>a b : α<GOAL>(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
<VAR>α : Type u<VAR>CommSemiring α<VAR>a b : α<GOAL>(a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b
<VAR>α : Type u_1<VAR>Mul α<VAR>self : HasDistribNeg α<VAR>x y : α<GOAL>x * -y = -(x * y)
<VAR>α : Type u_1<VAR>Mul α<VAR>self : HasDistribNeg α<VAR>x y : α<GOAL>-x * y = -(x * y)
<VAR>α : Type u<VAR>Mul α<VAR>HasDistribNeg α<VAR>a b : α<GOAL>-a * b = -(a * b)
<VAR>α : Type u<VAR>Mul α<VAR>HasDistribNeg α<VAR>a b : α<GOAL>a * -b = -(a * b)
<VAR>α : Type u<VAR>Mul α<VAR>HasDistribNeg α<VAR>a b : α<GOAL>-a * -b = a * b
<VAR>α : Type u<VAR>Mul α<VAR>HasDistribNeg α<VAR>a b : α<GOAL>-(a * b) = -a * b
<VAR>α : Type u<VAR>Mul α<VAR>HasDistribNeg α<VAR>a b : α<GOAL>-(a * b) = a * -b
<VAR>α : Type u<VAR>Mul α<VAR>HasDistribNeg α<VAR>a b : α<GOAL>-a * b = a * -b
<VAR>α : Type u<VAR>MulOneClass α<VAR>HasDistribNeg α<VAR>a : α<GOAL>-a = -1 * a
<VAR>α : Type u<VAR>MulOneClass α<VAR>HasDistribNeg α<VAR>a : α<GOAL>a * -1 = -a
<VAR>α : Type u<VAR>MulOneClass α<VAR>HasDistribNeg α<VAR>a : α<GOAL>-1 * a = -a
<VAR>α : Type u<VAR>NonUnitalNonAssocRing α<VAR>a b c : α<GOAL>a * (b - c) = a * b - a * c
<VAR>α : Type u<VAR>NonUnitalNonAssocRing α<VAR>a b c : α<GOAL>(a - b) * c = a * c - b * c
<VAR>α : Type u<VAR>NonAssocRing α<VAR>a b : α<GOAL>(a - 1) * b = a * b - b
<VAR>α : Type u<VAR>NonAssocRing α<VAR>a b : α<GOAL>a * (b - 1) = a * b - a
<VAR>α : Type u<VAR>NonAssocRing α<VAR>a b : α<GOAL>(1 - a) * b = b - a * b
<VAR>α : Type u<VAR>NonAssocRing α<VAR>a b : α<GOAL>a * (1 - b) = a - a * b
<VAR>R : Type x<VAR>Distrib R<VAR>a b c : R<GOAL>Commute a b → Commute a c → Commute a (b + c)
<VAR>R : Type x<VAR>Distrib R<VAR>a b c : R<GOAL>Commute a c → Commute b c → Commute (a + b) c
<VAR>R : Type x<VAR>NonUnitalNonAssocRing R<VAR>a b : R<VAR>h : Commute a b<GOAL>a * a - b * b = (a + b) * (a - b)
<VAR>R : Type x<VAR>NonUnitalNonAssocRing R<VAR>a b : R<VAR>h : Commute a b<GOAL>a * a - b * b = (a - b) * (a + b)
<VAR>R : Type x<VAR>NonUnitalNonAssocRing R<VAR>NoZeroDivisors R<VAR>a b : R<VAR>h : Commute a b<GOAL>a * a = b * b ↔ a = b ∨ a = -b
<VAR>R : Type x<VAR>Mul R<VAR>HasDistribNeg R<VAR>a b : R<GOAL>Commute a b → Commute a (-b)
<VAR>R : Type x<VAR>Mul R<VAR>HasDistribNeg R<VAR>a b : R<GOAL>Commute a (-b) ↔ Commute a b
<VAR>R : Type x<VAR>Mul R<VAR>HasDistribNeg R<VAR>a b : R<GOAL>Commute a b → Commute (-a) b
<VAR>R : Type x<VAR>Mul R<VAR>HasDistribNeg R<VAR>a b : R<GOAL>Commute (-a) b ↔ Commute a b
<VAR>R : Type x<VAR>MulOneClass R<VAR>HasDistribNeg R<VAR>a : R<GOAL>Commute a (-1)
<VAR>R : Type x<VAR>MulOneClass R<VAR>HasDistribNeg R<VAR>a : R<GOAL>Commute (-1) a
<VAR>R : Type x<VAR>NonUnitalNonAssocRing R<VAR>a b c : R<GOAL>Commute a b → Commute a c → Commute a (b - c)
<VAR>R : Type x<VAR>NonUnitalNonAssocRing R<VAR>a b c : R<GOAL>Commute a c → Commute b c → Commute (a - b) c
<VAR>R : Type x<VAR>Ring R<VAR>a b : R<VAR>h : Commute a b<GOAL>a ^ 2 - b ^ 2 = (a + b) * (a - b)
<VAR>R : Type x<VAR>Ring R<VAR>a b : R<VAR>NoZeroDivisors R<VAR>h : Commute a b<GOAL>a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
<VAR>R : Type x<VAR>Monoid R<VAR>HasDistribNeg R<VAR>n : ℕ<GOAL>(-1) ^ n = 1 ∨ (-1) ^ n = -1
<VAR>R : Type x<VAR>Monoid R<VAR>HasDistribNeg R<VAR>a : R<VAR>n : ℕ<GOAL>(-a) ^ n = (-1) ^ n * a ^ n
<VAR>R : Type x<VAR>Monoid R<VAR>HasDistribNeg R<VAR>a : R<VAR>n : ℕ<GOAL>(-a) ^ n = a ^ n * (-1) ^ n
<VAR>R : Type x<VAR>Monoid R<VAR>HasDistribNeg R<VAR>a : R<GOAL>(-a) ^ 2 = a ^ 2
<VAR>R : Type x<VAR>Monoid R<VAR>HasDistribNeg R<GOAL>(-1) ^ 2 = 1
<VAR>R : Type x<VAR>Ring R<VAR>a : R<VAR>n : ℕ<GOAL>(-1) ^ n * a = 0 ↔ a = 0
<VAR>R : Type x<VAR>Ring R<VAR>a : R<VAR>n : ℕ<GOAL>a * (-1) ^ n = 0 ↔ a = 0
<VAR>R : Type x<VAR>Ring R<VAR>n : ℕ<GOAL>(-1) ^ n = (-1) ^ (n % 2)
<VAR>R : Type x<VAR>Ring R<VAR>a : R<VAR>NoZeroDivisors R<GOAL>a ^ 2 = 1 ↔ a = 1 ∨ a = -1
<VAR>R : Type x<VAR>Ring R<VAR>a : R<VAR>NoZeroDivisors R<GOAL>a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1
<VAR>R : Type x<VAR>CommRing R<VAR>a b : R<GOAL>a * a - b * b = (a + b) * (a - b)
<VAR>R : Type x<VAR>NonAssocRing R<VAR>a : R<GOAL>a * a - 1 = (a + 1) * (a - 1)
<VAR>R : Type x<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>a b : R<GOAL>a * a = b * b ↔ a = b ∨ a = -b
<VAR>R : Type x<VAR>NonAssocRing R<VAR>NoZeroDivisors R<VAR>a : R<GOAL>a * a = 1 ↔ a = 1 ∨ a = -1
<VAR>R : Type x<VAR>CommRing R<VAR>a b : R<GOAL>a ^ 2 - b ^ 2 = (a + b) * (a - b)
<VAR>R : Type x<VAR>CommRing R<VAR>a b : R<GOAL>(a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
<VAR>R : Type x<VAR>CommRing R<VAR>a b : R<GOAL>(a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b
<VAR>R : Type x<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>a b : R<GOAL>a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
<VAR>R : Type x<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>a b : R<GOAL>a ^ 2 = b ^ 2 → a = b ∨ a = -b
<VAR>R : Type x<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>a b : Rˣ<GOAL>a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
<VAR>R : Type x<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>a b : Rˣ<VAR>h : a ^ 2 = b ^ 2<GOAL>a = b ∨ a = -b
<VAR>R : Type x<VAR>Ring R<VAR>NoZeroDivisors R<VAR>u : Rˣ<GOAL>u⁻¹ = u ↔ u = 1 ∨ u = -1
<VAR>R : Type x<VAR>NonUnitalNonAssocRing R<VAR>x y : R<GOAL>⁅x, y⁆ = x * y - y * x
<VAR>R : Type x<VAR>NonUnitalNonAssocRing R<VAR>x y : R<GOAL>Commute x y ↔ ⁅x, y⁆ = 0
<VAR>R : Type x<VAR>NonUnitalNonAssocRing R<VAR>x y : R<VAR>h : Commute x y<GOAL>⁅x, y⁆ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>SMul M R<VAR>Semigroup R<VAR>SMulCommClass M R R<VAR>x y : R<VAR>m : M<VAR>h : x ∣ y<GOAL>x ∣ m • y
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>x y : R<VAR>n : ℕ<VAR>h : x ∣ y<GOAL>x ∣ n • y
<VAR>R : Type u_1<VAR>NonUnitalRing R<VAR>x y : R<VAR>z : ℤ<VAR>h : x ∣ y<GOAL>x ∣ z • y
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>Semiring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hy : y ^ n = 0<GOAL>x ^ m ∣ (x + y) ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>Semiring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hx : x ^ n = 0<GOAL>y ^ m ∣ (x + y) ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>h : (x - y) ^ n = 0<GOAL>x ^ m ∣ y ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>h : (x + y) ^ n = 0<GOAL>x ^ m ∣ y ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hy : y ^ n = 0<GOAL>x ^ m ∣ (x - y) ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hx : x ^ n = 0<GOAL>y ^ m ∣ (x - y) ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hx : x ^ n = 0<GOAL>(x + y) ^ m ∣ y ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hy : y ^ n = 0<GOAL>(x + y) ^ m ∣ x ^ p
<VAR>R : Type u_1<VAR>CommRing R<VAR>p a b c d x y : R<VAR>h1 : p ∣ a * x + b * y<VAR>h2 : p ∣ c * x + d * y<GOAL>p ∣ (a * d - b * c) * x
<VAR>R : Type u_1<VAR>CommRing R<VAR>p a b c d x y : R<VAR>h1 : p ∣ a * x + b * y<VAR>h2 : p ∣ c * x + d * y<GOAL>p ∣ (a * d - b * c) * y
<VAR>R : Type u_1<VAR>CommRing R<VAR>p a b c d x y : R<VAR>IsDomain R<VAR>GCDMonoid R<VAR>h1 : p ∣ a * x + b * y<VAR>h2 : p ∣ c * x + d * y<GOAL>p ∣ (a * d - b * c) * gcd x y
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<GOAL>⇑(NonUnitalRingHom.fst R S) = Prod.fst
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<GOAL>⇑(NonUnitalRingHom.snd R S) = Prod.snd
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>T : Type u_7<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring T<VAR>f : R →ₙ+* S<VAR>g : R →ₙ+* T<VAR>x : R<GOAL>(f.prod g) x = (f x, g x)