ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>m n : σ →₀ ℕ<VAR>a b : R<GOAL>(MvPowerSeries.monomial R m) a * (MvPowerSeries.monomial R n) b = (MvPowerSeries.monomial R (m + n)) (a * b)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<GOAL>⇑(MvPowerSeries.monomial R 0) = ⇑(MvPowerSeries.C σ R)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>a : R<GOAL>(MvPowerSeries.monomial R 0) a = (MvPowerSeries.C σ R) a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>DecidableEq σ<VAR>n : σ →₀ ℕ<VAR>a : R<GOAL>(MvPowerSeries.coeff R n) ((MvPowerSeries.C σ R) a) = if n = 0 then a else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>a : R<GOAL>(MvPowerSeries.coeff R 0) ((MvPowerSeries.C σ R) a) = a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>DecidableEq σ<VAR>n : σ →₀ ℕ<VAR>s : σ<GOAL>(MvPowerSeries.coeff R n) (MvPowerSeries.X s) = if n = Finsupp.single s 1 then 1 else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>DecidableEq σ<VAR>s t : σ<GOAL>(MvPowerSeries.coeff R (Finsupp.single t 1)) (MvPowerSeries.X s) = if t = s then 1 else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>s : σ<GOAL>(MvPowerSeries.coeff R (Finsupp.single s 1)) (MvPowerSeries.X s) = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>s : σ<GOAL>(MvPowerSeries.coeff R 0) (MvPowerSeries.X s) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<VAR>s : σ<GOAL>Commute φ (MvPowerSeries.X s)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>s : σ<GOAL>MvPowerSeries.X s = (MvPowerSeries.monomial R (Finsupp.single s 1)) 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>s : σ<VAR>n : ℕ<GOAL>MvPowerSeries.X s ^ n = (MvPowerSeries.monomial R (Finsupp.single s n)) 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>DecidableEq σ<VAR>m : σ →₀ ℕ<VAR>s : σ<VAR>n : ℕ<GOAL>(MvPowerSeries.coeff R m) (MvPowerSeries.X s ^ n) = if m = Finsupp.single s n then 1 else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<VAR>a : R<GOAL>(MvPowerSeries.coeff R n) (φ * (MvPowerSeries.C σ R) a) = (MvPowerSeries.coeff R n) φ * a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<VAR>a : R<GOAL>(MvPowerSeries.coeff R n) ((MvPowerSeries.C σ R) a * φ) = a * (MvPowerSeries.coeff R n) φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<VAR>s : σ<GOAL>(MvPowerSeries.coeff R 0) (φ * MvPowerSeries.X s) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<VAR>s : σ<GOAL>(MvPowerSeries.coeff R 0) (MvPowerSeries.X s * φ) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<GOAL>⇑(MvPowerSeries.coeff R 0) = ⇑(MvPowerSeries.constantCoeff σ R)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<GOAL>(MvPowerSeries.coeff R 0) φ = (MvPowerSeries.constantCoeff σ R) φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>a : R<GOAL>(MvPowerSeries.constantCoeff σ R) ((MvPowerSeries.C σ R) a) = a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<GOAL>(MvPowerSeries.constantCoeff σ R).comp (MvPowerSeries.C σ R) = RingHom.id R
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<GOAL>(MvPowerSeries.constantCoeff σ R) 0 = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<GOAL>(MvPowerSeries.constantCoeff σ R) 1 = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>s : σ<GOAL>(MvPowerSeries.constantCoeff σ R) (MvPowerSeries.X s) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<VAR>h : IsUnit φ<GOAL>IsUnit ((MvPowerSeries.constantCoeff σ R) φ)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>f : MvPowerSeries σ R<VAR>n : σ →₀ ℕ<VAR>a : R<GOAL>(MvPowerSeries.coeff R n) (a • f) = a * (MvPowerSeries.coeff R n) f
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>f : MvPowerSeries σ R<VAR>a : R<GOAL>a • f = (MvPowerSeries.C σ R) a * f
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>Nontrivial R<VAR>s t : σ<GOAL>MvPowerSeries.X s = MvPowerSeries.X t ↔ s = t
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<GOAL>MvPowerSeries.map σ (RingHom.id R) = RingHom.id (MvPowerSeries σ R)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>T : Type u_4<VAR>Semiring R<VAR>Semiring S<VAR>Semiring T<VAR>f : R →+* S<VAR>g : S →+* T<GOAL>MvPowerSeries.map σ (g.comp f) = (MvPowerSeries.map σ g).comp (MvPowerSeries.map σ f)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<GOAL>(MvPowerSeries.coeff S n) ((MvPowerSeries.map σ f) φ) = f ((MvPowerSeries.coeff R n) φ)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>φ : MvPowerSeries σ R<GOAL>(MvPowerSeries.constantCoeff σ S) ((MvPowerSeries.map σ f) φ) = f ((MvPowerSeries.constantCoeff σ R) φ)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>n : σ →₀ ℕ<VAR>a : R<GOAL>(MvPowerSeries.map σ f) ((MvPowerSeries.monomial R n) a) = (MvPowerSeries.monomial S n) (f a)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>a : R<GOAL>(MvPowerSeries.map σ f) ((MvPowerSeries.C σ R) a) = (MvPowerSeries.C σ S) (f a)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>s : σ<GOAL>(MvPowerSeries.map σ f) (MvPowerSeries.X s) = MvPowerSeries.X s
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>s : σ<VAR>n : ℕ<VAR>φ : MvPowerSeries σ R<GOAL>MvPowerSeries.X s ^ n ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s < n → (MvPowerSeries.coeff R m) φ = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>s : σ<VAR>φ : MvPowerSeries σ R<GOAL>MvPowerSeries.X s ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (MvPowerSeries.coeff R m) φ = 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>DecidableEq σ<VAR>f : ι → MvPowerSeries σ R<VAR>d : σ →₀ ℕ<VAR>s : Finset ι<GOAL>(MvPowerSeries.coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (MvPowerSeries.coeff R (l i)) (f i)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>n : ℕ<VAR>d : σ →₀ ℕ<GOAL>(MvPowerSeries.coeff R d) (f ^ n) = ∑ l ∈ (Finset.range n).finsuppAntidiag d, ∏ i ∈ Finset.range n, (MvPowerSeries.coeff R (l i)) f
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (MvPowerSeries.constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<GOAL>(MvPowerSeries.coeff R d) (f ^ n) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>MvPowerSeries.C σ R = algebraMap R (MvPowerSeries σ R)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(algebraMap R (MvPowerSeries σ A)) r = (MvPowerSeries.C σ A) ((algebraMap R A) r)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<GOAL>↑φ = fun n => MvPolynomial.coeff n φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>n : σ →₀ ℕ<GOAL>(MvPowerSeries.coeff R n) ↑φ = MvPolynomial.coeff n φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : σ →₀ ℕ<VAR>a : R<GOAL>↑((MvPolynomial.monomial n) a) = (MvPowerSeries.monomial R n) a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>↑0 = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>↑1 = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ ψ : MvPolynomial σ R<GOAL>↑(φ + ψ) = ↑φ + ↑ψ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ ψ : MvPolynomial σ R<GOAL>↑(φ * ψ) = ↑φ * ↑ψ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>a : R<GOAL>↑(MvPolynomial.C a) = (MvPowerSeries.C σ R) a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>s : σ<GOAL>↑(MvPolynomial.X s) = MvPowerSeries.X s
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>Function.Injective Coe.coe
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ ψ : MvPolynomial σ R<GOAL>↑φ = ↑ψ ↔ φ = ψ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<GOAL>↑φ = 0 ↔ φ = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<GOAL>↑φ = 1 ↔ φ = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>n : ℕ<GOAL>↑(φ ^ n) = ↑φ ^ n
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<GOAL>MvPolynomial.coeToMvPowerSeries.ringHom φ = ↑φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>A : Type u_3<VAR>CommSemiring A<VAR>Algebra R A<GOAL>(MvPolynomial.coeToMvPowerSeries.algHom A) φ = (MvPowerSeries.map σ (algebraMap R A)) ↑φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>p : MvPolynomial σ R<GOAL>(algebraMap (MvPolynomial σ R) (MvPowerSeries σ A)) p = (MvPowerSeries.map σ (algebraMap R A)) ↑p
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>f : MvPowerSeries σ R<GOAL>(algebraMap (MvPowerSeries σ R) (MvPowerSeries σ A)) f = (MvPowerSeries.map σ (algebraMap R A)) f
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>IsDomain k<VAR>CharP k p<VAR>PerfectRing k p<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>WittVector.Isocrystal p k V<VAR>V₂ : Type u_3<VAR>AddCommGroup V₂<VAR>WittVector.Isocrystal p k V₂<VAR>self : WittVector.IsocrystalHom p k V V₂<VAR>x : V<GOAL>(WittVector.Isocrystal.frobenius p k) (self.toLinearMap x) = self.toLinearMap ((WittVector.Isocrystal.frobenius p k) x)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>IsDomain k<VAR>CharP k p<VAR>PerfectRing k p<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>WittVector.Isocrystal p k V<VAR>V₂ : Type u_3<VAR>AddCommGroup V₂<VAR>WittVector.Isocrystal p k V₂<VAR>self : WittVector.IsocrystalEquiv p k V V₂<VAR>x : V<GOAL>(WittVector.Isocrystal.frobenius p k) (self.toLinearEquiv x) = self.toLinearEquiv ((WittVector.Isocrystal.frobenius p k) x)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>IsDomain k<VAR>CharP k p<VAR>PerfectRing k p<VAR>m : ℤ<VAR>x : WittVector.StandardOneDimIsocrystal p k m<GOAL>(WittVector.Isocrystal.frobenius p k) x = ↑p ^ m • (WittVector.FractionRing.frobeniusRingHom p k) x
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>k : Type u_2<VAR>Field k<VAR>IsAlgClosed k<VAR>CharP k p<VAR>V : Type u_3<VAR>AddCommGroup V<VAR>WittVector.Isocrystal p k V<VAR>h_dim : FiniteDimensional.finrank (FractionRing (WittVector p k)) V = 1<GOAL>∃ m, Nonempty (WittVector.IsocrystalEquiv p k (WittVector.StandardOneDimIsocrystal p k m) V)
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>Fact (Nat.Prime p)<VAR>f g : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (MvPolynomial.bind₁ f) (wittPolynomial p ℤ n) = (MvPolynomial.bind₁ g) (wittPolynomial p ℤ n)<GOAL>f = g
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f g : ℕ → MvPolynomial ℕ ℤ<VAR>h : ∀ (n : ℕ), (MvPolynomial.bind₁ f) (wittPolynomial p ℤ n) = (MvPolynomial.bind₁ g) (wittPolynomial p ℤ n)<GOAL>f = g
<VAR>p : ℕ<VAR>f : ⦃R : Type u_3⦄ → [inst : CommRing R] → WittVector p R → WittVector p R<VAR>self : WittVector.IsPoly p f<GOAL>∃ φ, ∀ ⦃R : Type u_3⦄ [inst : CommRing R] (x : WittVector p R), (f x).coeff = fun n => (MvPolynomial.aeval x.coeff) (φ n)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f g : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R<VAR>hf : WittVector.IsPoly p f<VAR>hg : WittVector.IsPoly p g<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x : WittVector p R) (n : ℕ), (WittVector.ghostComponent n) (f x) = (WittVector.ghostComponent n) (g x)<VAR>R : Type u<VAR>_Rcr : CommRing R<VAR>x : WittVector p R<GOAL>f x = g x
<VAR>p : ℕ<VAR>f : ⦃R : Type u_3⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R<VAR>self : WittVector.IsPoly₂ p f<GOAL>∃ φ, ∀ ⦃R : Type u_3⦄ [inst : CommRing R] (x y : WittVector p R), (f x y).coeff = fun n => WittVector.peval (φ n) ![x.coeff, y.coeff]
<VAR>p : ℕ<VAR>R : Type u<VAR>CommRing R<VAR>Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(MvPolynomial.bind₁ 0) (wittPolynomial p R n) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(MvPolynomial.bind₁ WittVector.onePoly) (wittPolynomial p ℤ n) = 1
<VAR>p : ℕ<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>Fact (Nat.Prime p)<VAR>f : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R<VAR>hf : WittVector.IsPoly p f<VAR>g : R →+* S<VAR>x : WittVector p R<GOAL>(WittVector.map g) (f x) = f ((WittVector.map g) x)
<VAR>p : ℕ<VAR>g : ⦃R : Type u_3⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R<VAR>f : ⦃R : Type u_3⦄ → [inst : CommRing R] → WittVector p R → WittVector p R<VAR>WittVector.IsPoly₂ p g<VAR>WittVector.IsPoly p f<GOAL>WittVector.IsPoly₂ p fun _R _Rcr x y => g (f x) y
<VAR>p : ℕ<VAR>g : ⦃R : Type u_3⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R<VAR>f : ⦃R : Type u_3⦄ → [inst : CommRing R] → WittVector p R → WittVector p R<VAR>WittVector.IsPoly₂ p g<VAR>WittVector.IsPoly p f<GOAL>WittVector.IsPoly₂ p fun _R _Rcr x y => g x (f y)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f g : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R<VAR>hf : WittVector.IsPoly₂ p f<VAR>hg : WittVector.IsPoly₂ p g<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : WittVector p R) (n : ℕ), (WittVector.ghostComponent n) (f x y) = (WittVector.ghostComponent n) (g x y)<VAR>R : Type u<VAR>_Rcr : CommRing R<VAR>x y : WittVector p R<GOAL>f x y = g x y
<VAR>p : ℕ<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>Fact (Nat.Prime p)<VAR>f : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R<VAR>hf : WittVector.IsPoly₂ p f<VAR>g : R →+* S<VAR>x y : WittVector p R<GOAL>(WittVector.map g) (f x y) = f ((WittVector.map g) x) ((WittVector.map g) y)
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>SetLike S R<VAR>hSR : NonUnitalSubringClass S R<VAR>s : S<GOAL>⇑(NonUnitalSubringClass.subtype s) = Subtype.val
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x : R<GOAL>x ∈ s.toNonUnitalSubsemiring ↔ x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>S : NonUnitalSubsemiring R<VAR>x : R<VAR>h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier<GOAL>x ∈ { toNonUnitalSubsemiring := S, neg_mem' := h } ↔ x ∈ S
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>S : NonUnitalSubsemiring R<VAR>h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier<GOAL>↑{ toNonUnitalSubsemiring := S, neg_mem' := h } = ↑S
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>S S' : NonUnitalSubsemiring R<VAR>h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier<VAR>h' : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier<GOAL>{ toNonUnitalSubsemiring := S, neg_mem' := h } ≤ { toNonUnitalSubsemiring := S', neg_mem' := h' } ↔ S ≤ S'
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>S T : NonUnitalSubring R<VAR>h : ∀ (x : R), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>S : NonUnitalSubring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>S : NonUnitalSubring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>Function.Injective NonUnitalSubring.toNonUnitalSubsemiring
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>StrictMono NonUnitalSubring.toNonUnitalSubsemiring
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>Monotone NonUnitalSubring.toNonUnitalSubsemiring
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>Function.Injective NonUnitalSubring.toAddSubgroup
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>StrictMono NonUnitalSubring.toAddSubgroup
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>Monotone NonUnitalSubring.toAddSubgroup
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>Function.Injective NonUnitalSubring.toSubsemigroup
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>StrictMono NonUnitalSubring.toSubsemigroup
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>Monotone NonUnitalSubring.toSubsemigroup
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>sm : Subsemigroup R<VAR>hm : ↑sm = s<VAR>sa : AddSubgroup R<VAR>ha : ↑sa = s<GOAL>↑(NonUnitalSubring.mk' s sm sa hm ha) = s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>sm : Subsemigroup R<VAR>hm : ↑sm = s<VAR>sa : AddSubgroup R<VAR>ha : ↑sa = s<VAR>x : R<GOAL>x ∈ NonUnitalSubring.mk' s sm sa hm ha ↔ x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>sm : Subsemigroup R<VAR>hm : ↑sm = s<VAR>sa : AddSubgroup R<VAR>ha : ↑sa = s<GOAL>(NonUnitalSubring.mk' s sm sa hm ha).toSubsemigroup = sm
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>sm : Subsemigroup R<VAR>hm : ↑sm = s<VAR>sa : AddSubgroup R<VAR>ha : ↑sa = s<GOAL>(NonUnitalSubring.mk' s sm sa hm ha).toAddSubgroup = sa
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<GOAL>0 ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x y : R<GOAL>x ∈ s → y ∈ s → x * y ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x y : R<GOAL>x ∈ s → y ∈ s → x + y ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x : R<GOAL>x ∈ s → -x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x y : R<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x - y ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>l : List R<GOAL>(∀ x ∈ l, x ∈ s) → l.sum ∈ s
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>m : Multiset R<GOAL>(∀ a ∈ m, a ∈ s) → m.sum ∈ s
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>ι : Type u_2<VAR>t : Finset ι<VAR>f : ι → R<VAR>h : ∀ c ∈ t, f c ∈ s<GOAL>∑ i ∈ t, f i ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x : R<VAR>hx : x ∈ s<VAR>n : ℤ<GOAL>n • x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x y : ↥s<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x : ↥s<GOAL>↑(-x) = -↑x
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x y : ↥s<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<GOAL>↑0 = 0
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x : ↥s<GOAL>↑x = 0 ↔ x = 0
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x : R<GOAL>x ∈ s.toSubsemigroup ↔ x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<GOAL>↑s.toSubsemigroup = ↑s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<VAR>x : R<GOAL>x ∈ s.toAddSubgroup ↔ x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<GOAL>↑s.toAddSubgroup = ↑s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<GOAL>↑s.toNonUnitalSubsemiring = ↑s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>x : R<GOAL>x ∈ ⊤
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>↑⊤ = Set.univ
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>x : R<GOAL>↑(NonUnitalSubring.topEquiv.symm x) = x
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>x : ↥⊤<GOAL>NonUnitalSubring.topEquiv x = ↑x
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s : NonUnitalSubring S<VAR>f : F<GOAL>↑(NonUnitalSubring.comap f s) = ⇑f ⁻¹' ↑s
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s : NonUnitalSubring S<VAR>f : F<VAR>x : R<GOAL>x ∈ NonUnitalSubring.comap f s ↔ f x ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>NonUnitalNonAssocRing T<VAR>s : NonUnitalSubring T<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<GOAL>NonUnitalSubring.comap f (NonUnitalSubring.comap g s) = NonUnitalSubring.comap (g.comp f) s
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>s : NonUnitalSubring R<GOAL>↑(NonUnitalSubring.map f s) = ⇑f '' ↑s
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>s : NonUnitalSubring R<VAR>y : S<GOAL>y ∈ NonUnitalSubring.map f s ↔ ∃ x ∈ s, f x = y
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<GOAL>NonUnitalSubring.map (NonUnitalRingHom.id R) s = s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>NonUnitalNonAssocRing T<VAR>s : NonUnitalSubring R<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<GOAL>NonUnitalSubring.map g (NonUnitalSubring.map f s) = NonUnitalSubring.map (g.comp f) s
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>s : NonUnitalSubring R<VAR>t : NonUnitalSubring S<GOAL>NonUnitalSubring.map f s ≤ t ↔ s ≤ NonUnitalSubring.comap f t
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<GOAL>GaloisConnection (NonUnitalSubring.map f) (NonUnitalSubring.comap f)
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s : NonUnitalSubring R<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>x : ↥s<GOAL>↑((s.equivMapOfInjective f hf) x) = f ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<GOAL>↑f.range = Set.range ⇑f
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<VAR>y : S<GOAL>y ∈ f.range ↔ ∃ x, f x = y
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<GOAL>f.range = NonUnitalSubring.map f ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<VAR>x : R<GOAL>f x ∈ f.range
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>NonUnitalNonAssocRing T<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<GOAL>NonUnitalSubring.map g f.range = (g.comp f).range
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>↑⊥ = {0}
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>x : R<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>p p' : NonUnitalSubring R<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>p p' : NonUnitalSubring R<VAR>x : R<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>S : Set (NonUnitalSubring R)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>S : Set (NonUnitalSubring R)<VAR>x : R<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>ι : Sort u_2<VAR>S : ι → NonUnitalSubring R<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>ι : Sort u_2<VAR>S : ι → NonUnitalSubring R<VAR>x : R<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set (NonUnitalSubring R)<GOAL>(sInf s).toSubsemigroup = ⨅ t ∈ s, t.toSubsemigroup
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set (NonUnitalSubring R)<GOAL>(sInf s).toAddSubgroup = ⨅ t ∈ s, t.toAddSubgroup
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>A : NonUnitalSubring R<GOAL>A = ⊤ ↔ ∀ (x : R), x ∈ A
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>↑(NonUnitalSubring.center R) = Set.center R
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>(NonUnitalSubring.center R).toNonUnitalSubsemiring = NonUnitalSubsemiring.center R
<VAR>R : Type u<VAR>NonUnitalRing R<VAR>z : R<GOAL>z ∈ NonUnitalSubring.center R ↔ ∀ (g : R), g * z = z * g
<VAR>R : Type u_1<VAR>NonUnitalCommRing R<GOAL>NonUnitalSubring.center R = ⊤
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>x : R<VAR>s : Set R<GOAL>x ∈ NonUnitalSubring.closure s ↔ ∀ (S : NonUnitalSubring R), s ⊆ ↑S → x ∈ S
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<GOAL>s ⊆ ↑(NonUnitalSubring.closure s)