ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalCommSemiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalCommSemiring R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<GOAL>Function.Injective (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing R)
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalNonAssocCommRing R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalNonAssocCommRing R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<GOAL>Function.Injective (@NonUnitalCommRing.toNonUnitalRing R)
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalCommRing R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalCommRing R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<GOAL>Function.Injective (@CommSemiring.toSemiring R)
<VAR>R : Type u<VAR>inst₁ inst₂ : CommSemiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : CommSemiring R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<GOAL>Function.Injective (@CommRing.toRing R)
<VAR>R : Type u<VAR>inst₁ inst₂ : CommRing R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : CommRing R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>α : Type u<VAR>Monoid α<VAR>HasDistribNeg α<VAR>u : αˣ<GOAL>↑(-u) = -↑u
<VAR>α : Type u<VAR>Monoid α<VAR>HasDistribNeg α<GOAL>↑(-1) = -1
<VAR>α : Type u<VAR>Monoid α<VAR>HasDistribNeg α<VAR>a : α<VAR>u : αˣ<GOAL>-(a /ₚ u) = -a /ₚ u
<VAR>α : Type u<VAR>Ring α<VAR>a b : α<VAR>u : αˣ<GOAL>a /ₚ u + b /ₚ u = (a + b) /ₚ u
<VAR>α : Type u<VAR>Ring α<VAR>a b : α<VAR>u : αˣ<GOAL>a /ₚ u - b /ₚ u = (a - b) /ₚ u
<VAR>α : Type u<VAR>Ring α<VAR>a b : α<VAR>u : αˣ<GOAL>a + b /ₚ u = (a * ↑u + b) /ₚ u
<VAR>α : Type u<VAR>Ring α<VAR>a b : α<VAR>u : αˣ<GOAL>a - b /ₚ u = (a * ↑u - b) /ₚ u
<VAR>α : Type u<VAR>Ring α<VAR>a b : α<VAR>u : αˣ<GOAL>a /ₚ u + b = (a + b * ↑u) /ₚ u
<VAR>α : Type u<VAR>Ring α<VAR>a b : α<VAR>u : αˣ<GOAL>a /ₚ u - b = (a - b * ↑u) /ₚ u
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>F : Type u_1<VAR>Ring β<VAR>FunLike F α β<VAR>RingHomClass F α β<VAR>f : F<VAR>u : αˣ<GOAL>(Units.map ↑f) (-u) = -(Units.map ↑f) u
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>F : Type u_1<VAR>Ring β<VAR>FunLike F α β<VAR>RingHomClass F α β<VAR>f : F<GOAL>(Units.map ↑f) (-1) = -1
<VAR>α : Type u<VAR>Monoid α<VAR>HasDistribNeg α<VAR>a : α<GOAL>IsUnit a → IsUnit (-a)
<VAR>α : Type u<VAR>Monoid α<VAR>HasDistribNeg α<VAR>a : α<GOAL>IsUnit (-a) ↔ IsUnit a
<VAR>α : Type u<VAR>Monoid α<VAR>HasDistribNeg α<GOAL>IsUnit (-1)
<VAR>α : Type u<VAR>Ring α<VAR>x y : α<GOAL>IsUnit (x - y) ↔ IsUnit (y - x)
<VAR>α : Type u<VAR>CommRing α<VAR>a b : α<VAR>u₁ u₂ : αˣ<GOAL>a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)
<VAR>α : Type u<VAR>CommRing α<VAR>a b : α<VAR>u₁ u₂ : αˣ<GOAL>a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)
<VAR>R : Type x<VAR>Semiring R<VAR>a : Rˣ<VAR>b : R<GOAL>↑a + b = ↑a * (1 + ↑a⁻¹ * b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Semigroup α<VAR>Semigroup β<VAR>F : Type u_3<VAR>EquivLike F α β<VAR>MulEquivClass F α β<VAR>f : F<VAR>a b : α<GOAL>f a ∣ f b ↔ a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Semigroup α<VAR>Semigroup β<VAR>F : Type u_3<VAR>EquivLike F α β<VAR>MulEquivClass F α β<VAR>f : F<VAR>DecompositionMonoid β<GOAL>DecompositionMonoid α
<VAR>α : Type u_1<VAR>Add α<VAR>Semigroup α<VAR>LeftDistribClass α<VAR>a b c : α<VAR>h₁ : a ∣ b<VAR>h₂ : a ∣ c<GOAL>a ∣ b + c
<VAR>α : Type u_1<VAR>Semiring α<VAR>a b c : α<VAR>m n : ℕ<VAR>ha : c ^ m ∣ a<VAR>hb : c ^ n ∣ b<GOAL>c ^ min m n ∣ a + b
<VAR>α : Type u_1<VAR>NonUnitalCommSemiring α<VAR>d x y : α<VAR>hdx : d ∣ x<VAR>hdy : d ∣ y<VAR>a b : α<GOAL>d ∣ a * x + b * y
<VAR>α : Type u_1<VAR>Semigroup α<VAR>HasDistribNeg α<VAR>a b : α<GOAL>a ∣ -b ↔ a ∣ b
<VAR>α : Type u_1<VAR>Semigroup α<VAR>HasDistribNeg α<VAR>a b : α<GOAL>-a ∣ b ↔ a ∣ b
<VAR>α : Type u_1<VAR>NonUnitalRing α<VAR>a b c : α<VAR>h₁ : a ∣ b<VAR>h₂ : a ∣ c<GOAL>a ∣ b - c
<VAR>α : Type u_1<VAR>NonUnitalRing α<VAR>a b c : α<VAR>h : a ∣ c<GOAL>a ∣ b + c ↔ a ∣ b
<VAR>α : Type u_1<VAR>NonUnitalRing α<VAR>a b c : α<VAR>h : a ∣ b<GOAL>a ∣ b + c ↔ a ∣ c
<VAR>α : Type u_1<VAR>NonUnitalRing α<VAR>a b c : α<VAR>h : a ∣ c<GOAL>a ∣ b - c ↔ a ∣ b
<VAR>α : Type u_1<VAR>NonUnitalRing α<VAR>a b c : α<VAR>h : a ∣ b<GOAL>a ∣ b - c ↔ a ∣ c
<VAR>α : Type u_1<VAR>NonUnitalRing α<VAR>a b c : α<VAR>h : a ∣ b - c<GOAL>a ∣ b ↔ a ∣ c
<VAR>α : Type u_1<VAR>NonUnitalRing α<VAR>a b c : α<GOAL>a ∣ b - c ↔ a ∣ c - b
<VAR>α : Type u_1<VAR>Ring α<VAR>a b : α<GOAL>a ∣ a + b ↔ a ∣ b
<VAR>α : Type u_1<VAR>Ring α<VAR>a b : α<GOAL>a ∣ b + a ↔ a ∣ b
<VAR>α : Type u_1<VAR>Ring α<VAR>a b : α<GOAL>a ∣ a - b ↔ a ∣ b
<VAR>α : Type u_1<VAR>Ring α<VAR>a b : α<GOAL>a ∣ b - a ↔ a ∣ b
<VAR>α : Type u_1<VAR>NonUnitalCommRing α<VAR>k a b x y : α<VAR>hab : k ∣ a - b<VAR>hxy : k ∣ x - y<GOAL>k ∣ a * x - b * y
<VAR>α : Type u_1<VAR>NonUnitalNonAssocRing α<VAR>k : α<VAR>h : ∀ (x : α), k * x = 0 → x = 0<GOAL>IsLeftRegular k
<VAR>α : Type u_1<VAR>NonUnitalNonAssocRing α<VAR>k : α<VAR>h : ∀ (x : α), x * k = 0 → x = 0<GOAL>IsRightRegular k
<VAR>α : Type u_1<VAR>NonUnitalNonAssocRing α<VAR>NoZeroDivisors α<VAR>k : α<VAR>hk : k ≠ 0<GOAL>IsRegular k
<VAR>α : Type u_1<VAR>Nontrivial α<VAR>NonUnitalNonAssocRing α<VAR>NoZeroDivisors α<VAR>k : α<GOAL>IsRegular k ↔ k ≠ 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>self : Subalgebra R A<VAR>r : R<GOAL>(algebraMap R A) r ∈ self.carrier
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : A<GOAL>x ∈ S.toSubsemiring ↔ x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Subalgebra R A<VAR>x : A<GOAL>x ∈ s.carrier ↔ x ∈ 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 : ∀ (x : A), x ∈ S ↔ x ∈ T<GOAL>S = T
<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.toSubsemiring = ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Function.Injective Subalgebra.toSubsemiring
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S U : Subalgebra R A<GOAL>S.toSubsemiring = U.toSubsemiring ↔ S = U
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>s : Set A<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>s : Set A<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>SetLike S A<VAR>OneMemClass S A<VAR>SMulMemClass S R A<VAR>s : S<VAR>r : R<GOAL>(algebraMap R A) r ∈ s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>r : R<GOAL>(algebraMap R A) r ∈ 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>(algebraMap R A).rangeS ≤ S.toSubsemiring
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>Set.range ⇑(algebraMap R A) ⊆ ↑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>Set.range ⇑(algebraMap R A) ≤ ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : A<VAR>hx : x ∈ S<VAR>r : R<GOAL>r • x ∈ 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>1 ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x y : A<VAR>hx : x ∈ S<VAR>hy : y ∈ S<GOAL>x * y ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : A<VAR>hx : x ∈ S<VAR>n : ℕ<GOAL>x ^ n ∈ 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>0 ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x y : A<VAR>hx : x ∈ S<VAR>hy : y ∈ S<GOAL>x + y ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : A<VAR>hx : x ∈ S<VAR>n : ℕ<GOAL>n • x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>n : ℕ<GOAL>↑n ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>L : List A<VAR>h : ∀ x ∈ L, x ∈ S<GOAL>L.prod ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>L : List A<VAR>h : ∀ x ∈ L, x ∈ S<GOAL>L.sum ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>m : Multiset A<VAR>h : ∀ x ∈ m, x ∈ S<GOAL>m.sum ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>ι : Type w<VAR>t : Finset ι<VAR>f : ι → A<VAR>h : ∀ x ∈ t, f x ∈ S<GOAL>∑ x ∈ t, f x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>m : Multiset A<VAR>h : ∀ x ∈ m, x ∈ S<GOAL>m.prod ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>ι : Type w<VAR>t : Finset ι<VAR>f : ι → A<VAR>h : ∀ x ∈ t, f x ∈ S<GOAL>∏ x ∈ t, f x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : A<VAR>hx : x ∈ S<GOAL>-x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x y : A<VAR>hx : x ∈ S<VAR>hy : y ∈ S<GOAL>x - y ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : A<VAR>hx : x ∈ S<VAR>n : ℤ<GOAL>n • x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>n : ℤ<GOAL>↑n ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : A<GOAL>x ∈ S.toSubring ↔ x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>↑S.toSubring = ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<GOAL>Function.Injective Subalgebra.toSubring
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S U : Subalgebra R A<GOAL>S.toSubring = U.toSubring ↔ S = U
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : A<GOAL>x ∈ Subalgebra.toSubmodule S ↔ x ∈ 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>↑(Subalgebra.toSubmodule S) = ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Function.Injective ⇑Subalgebra.toSubmodule
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x y : ↥S<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x y : ↥S<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>↑0 = 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>↑1 = 1
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : ↥S<GOAL>↑(-x) = -↑x
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x y : ↥S<GOAL>↑(x - y) = ↑x - ↑y
<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>Semiring R'<VAR>SMul R' R<VAR>Module R' A<VAR>IsScalarTower R' R A<VAR>r : R'<VAR>x : ↥S<GOAL>↑(r • x) = r • ↑x
<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>CommSemiring R'<VAR>SMul R' R<VAR>Algebra R' A<VAR>IsScalarTower R' R A<VAR>r : R'<GOAL>↑((algebraMap R' ↥S) r) = (algebraMap R' A) r
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : ↥S<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : ↥S<GOAL>↑x = 0 ↔ x = 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : ↥S<GOAL>↑x = 1 ↔ x = 1
<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 = Subtype.val
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : ↥S<GOAL>S.val x = ↑x
<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.subtype = ↑S.val
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.toSubring.subtype = ↑S.val
<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₁ S₂ : Subalgebra R A<VAR>f : A →ₐ[R] B<GOAL>S₁ ≤ S₂ → Subalgebra.map f S₁ ≤ 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>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (Subalgebra.map f)
<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.map (AlgHom.id R A) S = S
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>S : Subalgebra R A<VAR>g : B →ₐ[R] C<VAR>f : A →ₐ[R] B<GOAL>Subalgebra.map g (Subalgebra.map f S) = Subalgebra.map (g.comp 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>y : B<GOAL>y ∈ Subalgebra.map f S ↔ ∃ x ∈ S, f x = y
<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>Subalgebra.toSubmodule (Subalgebra.map f S) = Submodule.map f.toLinearMap (Subalgebra.toSubmodule 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<GOAL>(Subalgebra.map f S).toSubsemiring = Subsemiring.map f.toRingHom S.toSubsemiring
<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>↑(Subalgebra.map f S) = ⇑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>U : Subalgebra R B<GOAL>Subalgebra.map f S ≤ U ↔ S ≤ Subalgebra.comap f 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>f : A →ₐ[R] B<GOAL>GaloisConnection (Subalgebra.map f) (Subalgebra.comap 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>S : Subalgebra R B<VAR>f : A →ₐ[R] B<VAR>x : A<GOAL>x ∈ Subalgebra.comap f S ↔ f 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>S : Subalgebra R B<VAR>f : A →ₐ[R] B<GOAL>↑(Subalgebra.comap f S) = ⇑f ⁻¹' ↑S
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>SetLike S A<VAR>SubsemiringClass S A<VAR>hSR : SMulMemClass S R A<VAR>s : S<VAR>r : R<GOAL>↑((algebraMap R ↥s) r) = (algebraMap R A) r
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>SetLike S A<VAR>SubsemiringClass S A<VAR>hSR : SMulMemClass S R A<VAR>s : S<GOAL>⇑(SubalgebraClass.val s) = Subtype.val
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : Submodule R A<VAR>h_one : 1 ∈ p<VAR>h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p<VAR>x : A<GOAL>x ∈ p.toSubalgebra h_one h_mul ↔ x ∈ p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : Submodule R A<VAR>h_one : 1 ∈ p<VAR>h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p<GOAL>↑(p.toSubalgebra h_one h_mul) = ↑p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Submodule R A<VAR>h1 : 1 ∈ s<VAR>hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s<GOAL>s.toSubalgebra h1 hmul = { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : Submodule R A<VAR>h_one : 1 ∈ p<VAR>h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p<GOAL>Subalgebra.toSubmodule (p.toSubalgebra h_one h_mul) = p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>(Subalgebra.toSubmodule S).toSubalgebra ⋯ ⋯ = 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>φ : A →ₐ[R] B<VAR>y : B<GOAL>y ∈ φ.range ↔ ∃ x, φ x = y
<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>φ : A →ₐ[R] B<VAR>x : A<GOAL>φ x ∈ φ.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>φ : A →ₐ[R] B<GOAL>↑φ.range = Set.range ⇑φ
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : B →ₐ[R] C<GOAL>(g.comp f).range = Subalgebra.map g f.range
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : B →ₐ[R] C<GOAL>(g.comp f).range ≤ g.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<VAR>S : Subalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<GOAL>S.val.comp (f.codRestrict S hf) = 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<VAR>S : Subalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<VAR>x : A<GOAL>↑((f.codRestrict S hf) x) = f x
<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<VAR>S : Subalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<GOAL>Function.Injective ⇑(f.codRestrict S hf) ↔ Function.Injective ⇑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>Function.Surjective ⇑f.rangeRestrict
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>g : B → A<VAR>f : A →ₐ[R] B<VAR>h : Function.LeftInverse g ⇑f<VAR>x : A<GOAL>↑((AlgEquiv.ofLeftInverse h) x) = f x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>g : B → A<VAR>f : A →ₐ[R] B<VAR>h : Function.LeftInverse g ⇑f<VAR>x : ↥f.range<GOAL>(AlgEquiv.ofLeftInverse h).symm x = g ↑x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>x : A<GOAL>↑((AlgEquiv.ofInjective f hf) x) = f x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>e : A ≃ₐ[R] B<VAR>S : Subalgebra R A<VAR>y : ↑(⇑↑e.toRingEquiv.toAddEquiv '' ↑S.toAddSubmonoid)<GOAL>↑((e.subalgebraMap S).symm y) = (↑↑e).symm ↑y
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>e : A ≃ₐ[R] B<VAR>S : Subalgebra R A<VAR>x : ↑↑S.toAddSubmonoid<GOAL>↑((e.subalgebraMap S) x) = e ↑x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>GaloisConnection (Algebra.adjoin R) SetLike.coe
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>↑⊤ = Set.univ
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>x ∈ ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Subalgebra.toSubmodule ⊤ = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>⊤.toSubsemiring = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<GOAL>⊤.toSubring = ⊤
<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.toSubmodule S = ⊤ ↔ 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.toSubsemiring = ⊤ ↔ S = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.toSubring = ⊤ ↔ 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>x : A<GOAL>x ∈ S → x ∈ S ⊔ T
<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>x : A<GOAL>x ∈ T → x ∈ S ⊔ T
<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>x y : A<VAR>hx : x ∈ S<VAR>hy : y ∈ T<GOAL>x * y ∈ S ⊔ T
<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<VAR>S T : Subalgebra R A<GOAL>Subalgebra.map f (S ⊔ T) = Subalgebra.map f S ⊔ Subalgebra.map f T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<GOAL>↑(S ⊓ T) = ↑S ∩ ↑T
<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>x : A<GOAL>x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<GOAL>Subalgebra.toSubmodule (S ⊓ T) = Subalgebra.toSubmodule S ⊓ Subalgebra.toSubmodule T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<GOAL>(S ⊓ T).toSubsemiring = S.toSubsemiring ⊓ T.toSubsemiring
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Set (Subalgebra R A)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Set (Subalgebra R A)<VAR>x : A<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Set (Subalgebra R A)<GOAL>Subalgebra.toSubmodule (sInf S) = sInf (⇑Subalgebra.toSubmodule '' S)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Set (Subalgebra R A)<GOAL>(sInf S).toSubsemiring = sInf (Subalgebra.toSubsemiring '' S)
<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>↑(⨅ i, S i) = ⋂ i, ↑(S i)