ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>h : RingHomSurjective f<VAR>I : Ideal R<GOAL>Ideal.map f I = Submodule.map f.toSemilinearMap I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>hf : Function.Injective ⇑f<GOAL>Ideal.comap f ⊥ ≤ I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>Ideal.comap f ⊥ = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>f : R ≃+* S<GOAL>Ideal.map (↑f.symm) (Ideal.map (↑f) I) = I
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>f : R ≃+* S<GOAL>Ideal.comap (↑f) (Ideal.comap (↑f.symm) I) = I
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>f : R ≃+* S<GOAL>Ideal.map (↑f) I = Ideal.comap f.symm I
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>f : R ≃+* S<GOAL>Ideal.comap f.symm I = Ideal.map f I
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal S<VAR>f : R ≃+* S<GOAL>Ideal.map f.symm I = Ideal.comap f I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Ring R<VAR>Ring S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<GOAL>Ideal.comap f (Ideal.map f I) = I ⊔ Ideal.comap f ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Ring R<VAR>Ring S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>H : I.IsMaximal<GOAL>Ideal.map f I = ⊤ ∨ (Ideal.map f I).IsMaximal
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Ring R<VAR>Ring S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>K : Ideal S<VAR>H : K.IsMaximal<GOAL>(Ideal.comap f K).IsMaximal
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Ring R<VAR>Ring S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<GOAL>Ideal.comap f I ≤ Ideal.comap f J ↔ I ≤ J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Ring R<VAR>Ring S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>hf : Function.Bijective ⇑f<VAR>I : Ideal R<VAR>K : Ideal S<GOAL>Ideal.comap f K ≤ I ↔ K ≤ Ideal.map f I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Ring R<VAR>Ring S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>hf : Function.Bijective ⇑f<VAR>I : Ideal R<VAR>H : I.IsMaximal<GOAL>(Ideal.map f I).IsMaximal
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>e : R ≃+* S<GOAL>⊥.IsMaximal ↔ ⊥.IsMaximal
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<GOAL>Ideal.map f (I * J) = Ideal.map f I * Ideal.map f J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<GOAL>(Ideal.mapHom f) I = Ideal.map f I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>n : ℕ<GOAL>Ideal.map f (I ^ n) = Ideal.map f I ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K : Ideal S<GOAL>Ideal.comap f K.radical = (Ideal.comap f K).radical
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K : Ideal S<VAR>hK : K.IsRadical<GOAL>(Ideal.comap f K).IsRadical
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<GOAL>Ideal.map f I.radical ≤ (Ideal.map f I).radical
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K L : Ideal S<GOAL>Ideal.comap f K * Ideal.comap f L ≤ Ideal.comap f (K * L)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K : Ideal S<VAR>n : ℕ<GOAL>Ideal.comap f K ^ n ≤ Ideal.comap f (K ^ n)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rcf : RingHomClass F R S<VAR>f : F<VAR>r : R<GOAL>r ∈ RingHom.ker f ↔ f r = 0
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rcf : RingHomClass F R S<VAR>f : F<GOAL>↑(RingHom.ker f) = ⇑f ⁻¹' {0}
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rcf : RingHomClass F R S<VAR>f : F<GOAL>RingHom.ker f = Ideal.comap f ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>Semiring R<VAR>Semiring S<VAR>Semiring T<VAR>f : S →+* R<VAR>g : T →+* S<GOAL>Ideal.comap g (RingHom.ker f) = RingHom.ker (f.comp g)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rcf : RingHomClass F R S<VAR>Nontrivial S<VAR>f : F<GOAL>1 ∉ RingHom.ker f
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rcf : RingHomClass F R S<VAR>Nontrivial S<VAR>f : F<GOAL>RingHom.ker f ≠ ⊤
<VAR>S : Type v<VAR>Semiring S<VAR>ι : Type u_3<VAR>R : ι → Type u_4<VAR>(i : ι) → Semiring (R i)<VAR>φ : (i : ι) → S →+* R i<GOAL>RingHom.ker (Pi.ringHom φ) = ⨅ i, RingHom.ker (φ i)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<GOAL>RingHom.ker f.rangeSRestrict = RingHom.ker f
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Ring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<GOAL>Function.Injective ⇑f ↔ RingHom.ker f = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Ring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<GOAL>RingHom.ker f = ⊥ ↔ ∀ (x : R), f x = 0 → x = 0
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Semiring S<VAR>f : R ≃+* S<GOAL>RingHom.ker ↑f = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Semiring S<VAR>F' : Type u_2<VAR>EquivLike F' R S<VAR>RingEquivClass F' R S<VAR>f : F'<GOAL>RingHom.ker f = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Ring R<VAR>Ring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>x y : R<GOAL>x - y ∈ RingHom.ker f ↔ f x = f y
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>RingHom.ker f.rangeRestrict = RingHom.ker f
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Ring R<VAR>Ring S<VAR>IsDomain S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<GOAL>(RingHom.ker f).IsPrime
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>F : Type u_3<VAR>Ring R<VAR>Field K<VAR>FunLike F R K<VAR>RingHomClass F R K<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>(RingHom.ker f).IsMaximal
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>I : Ideal R<VAR>f : F<GOAL>Ideal.map f I = ⊥ ↔ I ≤ RingHom.ker f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>K : Ideal S<VAR>f : F<GOAL>RingHom.ker f ≤ Ideal.comap f K
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>F' : Type u_4<VAR>EquivLike F' R S<VAR>RingEquivClass F' R S<VAR>f : F'<VAR>I : Ideal R<VAR>I.IsPrime<GOAL>(Ideal.map f I).IsPrime
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>Ring R<VAR>Ring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>A : Set (Ideal R)<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>(∀ J ∈ A, RingHom.ker f ≤ J) → Ideal.map f (sInf A) = sInf (Ideal.map f '' A)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>Ring R<VAR>Ring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>H : I.IsPrime<VAR>hk : RingHom.ker f ≤ I<GOAL>(Ideal.map f I).IsPrime
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>Ring R<VAR>Ring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>I : Ideal R<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>Ideal.map f I = ⊥ ↔ I = ⊥
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>Ideal.map f I = Ideal.map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>h : RingHom.ker f ≤ I<GOAL>Ideal.map f I.radical = (Ideal.map f I).radical
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>Ring A<VAR>Ring B<VAR>Ring C<VAR>f : A →+* B<VAR>f_inv : B → A<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : A →+* C<VAR>hg : RingHom.ker f ≤ RingHom.ker g<VAR>a : A<GOAL>(f.liftOfRightInverseAux f_inv hf g hg) (f a) = g a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>Ring A<VAR>Ring B<VAR>Ring C<VAR>f : A →+* B<VAR>f_inv : B → A<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : { g // RingHom.ker f ≤ RingHom.ker g }<VAR>x : A<GOAL>((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>Ring A<VAR>Ring B<VAR>Ring C<VAR>f : A →+* B<VAR>f_inv : B → A<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : { g // RingHom.ker f ≤ RingHom.ker g }<GOAL>((f.liftOfRightInverse f_inv hf) g).comp f = ↑g
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>Ring A<VAR>Ring B<VAR>Ring C<VAR>f : A →+* B<VAR>f_inv : B → A<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : A →+* C<VAR>hg : RingHom.ker f ≤ RingHom.ker g<VAR>h : B →+* C<VAR>hh : h.comp f = g<GOAL>h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>RingHom.ker f = RingHom.ker ↑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>I : Ideal A<GOAL>Ideal.map f I = Ideal.map (↑f) I
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>Algebra R S<VAR>I : Ideal R<VAR>c : ↥I<GOAL>↑((Algebra.idealMap S I) c) = (algebraMap R S) ↑c
<VAR>lo hi : ℕ<VAR>a : ℕ<VAR>h : lo.succ ≤ a ∧ a ≤ hi<GOAL>lo ≤ a.pred ∧ a.pred < hi
<VAR>n : ℕ<GOAL>RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span {↑n}
<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>f g : R →+* ZMod n<VAR>h : RingHom.ker f = RingHom.ker g<GOAL>f = g
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>Module.Finite R B<VAR>x : B<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_5<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>HS : (Subalgebra.toSubmodule S).FG<VAR>x : A<VAR>hx : x ∈ S<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x y z : S<VAR>hx : f.IsIntegralElem x<VAR>hy : f.IsIntegralElem y<VAR>hz : z ∈ Subring.closure {x, y}<GOAL>f.IsIntegralElem z
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x y z : A<VAR>hx : IsIntegral R x<VAR>hy : IsIntegral R y<VAR>hz : z ∈ Subring.closure {x, y}<GOAL>IsIntegral R z
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x y : S<VAR>hx : f.IsIntegralElem x<VAR>hy : f.IsIntegralElem y<GOAL>f.IsIntegralElem (x + y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x y : A<VAR>hx : IsIntegral R x<VAR>hy : IsIntegral R y<GOAL>IsIntegral R (x + y)
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x : S<VAR>hx : f.IsIntegralElem x<GOAL>f.IsIntegralElem (-x)
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>x : B<VAR>hx : IsIntegral R x<GOAL>IsIntegral R (-x)
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x y : S<VAR>hx : f.IsIntegralElem x<VAR>hy : f.IsIntegralElem y<GOAL>f.IsIntegralElem (x - y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x y : A<VAR>hx : IsIntegral R x<VAR>hy : IsIntegral R y<GOAL>IsIntegral R (x - y)
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x y : S<VAR>hx : f.IsIntegralElem x<VAR>hy : f.IsIntegralElem y<GOAL>f.IsIntegralElem (x * y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x y : A<VAR>hx : IsIntegral R x<VAR>hy : IsIntegral R y<GOAL>IsIntegral R (x * y)
<VAR>B : Type u_3<VAR>S : Type u_4<VAR>Ring B<VAR>R : Type u_5<VAR>CommSemiring R<VAR>CommRing S<VAR>Algebra R B<VAR>Algebra S B<VAR>Algebra R S<VAR>IsScalarTower R S B<VAR>x : B<VAR>r : R<VAR>hx : IsIntegral S x<GOAL>IsIntegral S (r • x)
<VAR>S : Type u_1<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>SetLike S R<VAR>self : NonUnitalSubsemiringClass S R<VAR>s : S<VAR>a b : R<GOAL>a ∈ s → b ∈ s → a * b ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>SetLike S R<VAR>NonUnitalSubsemiringClass S R<VAR>s : S<GOAL>⇑(NonUnitalSubsemiringClass.subtype s) = Subtype.val
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<VAR>x : R<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>S T : NonUnitalSubsemiring R<VAR>h : ∀ (x : R), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>S : NonUnitalSubsemiring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>S : NonUnitalSubsemiring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>Function.Injective NonUnitalSubsemiring.toSubsemigroup
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>StrictMono NonUnitalSubsemiring.toSubsemigroup
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>Monotone NonUnitalSubsemiring.toSubsemigroup
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>Function.Injective NonUnitalSubsemiring.toAddSubmonoid
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>StrictMono NonUnitalSubsemiring.toAddSubmonoid
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>Monotone NonUnitalSubsemiring.toAddSubmonoid
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<VAR>sg : Subsemigroup R<VAR>hg : ↑sg = s<VAR>sa : AddSubmonoid R<VAR>ha : ↑sa = s<GOAL>↑(NonUnitalSubsemiring.mk' s sg hg sa ha) = s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<VAR>sg : Subsemigroup R<VAR>hg : ↑sg = s<VAR>sa : AddSubmonoid R<VAR>ha : ↑sa = s<VAR>x : R<GOAL>x ∈ NonUnitalSubsemiring.mk' s sg hg sa ha ↔ x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<VAR>sg : Subsemigroup R<VAR>hg : ↑sg = s<VAR>sa : AddSubmonoid R<VAR>ha : ↑sa = s<GOAL>(NonUnitalSubsemiring.mk' s sg hg sa ha).toSubsemigroup = sg
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<VAR>sg : Subsemigroup R<VAR>hg : ↑sg = s<VAR>sa : AddSubmonoid R<VAR>ha : ↑sa = s<GOAL>(NonUnitalSubsemiring.mk' s sg hg sa ha).toAddSubmonoid = sa
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<GOAL>↑0 = 0
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<VAR>x y : ↥s<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<VAR>x y : ↥s<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<VAR>x : R<GOAL>x ∈ s.toSubsemigroup ↔ x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<GOAL>↑s.toSubsemigroup = ↑s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<VAR>x : R<GOAL>x ∈ s.toAddSubmonoid ↔ x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<GOAL>↑s.toAddSubmonoid = ↑s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>x : R<GOAL>x ∈ ⊤
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>↑⊤ = Set.univ
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>x : ↥⊤<GOAL>NonUnitalSubsemiring.topEquiv x = ↑x
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>x : R<GOAL>↑(NonUnitalSubsemiring.topEquiv.symm x) = x
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s : NonUnitalSubsemiring S<VAR>f : F<GOAL>↑(NonUnitalSubsemiring.comap f s) = ⇑f ⁻¹' ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s : NonUnitalSubsemiring S<VAR>f : F<VAR>x : R<GOAL>x ∈ NonUnitalSubsemiring.comap f s ↔ f x ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>G : Type u_2<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>FunLike G S T<VAR>NonUnitalRingHomClass G S T<VAR>s : NonUnitalSubsemiring T<VAR>g : G<VAR>f : F<GOAL>NonUnitalSubsemiring.comap f (NonUnitalSubsemiring.comap g s) = NonUnitalSubsemiring.comap ((↑g).comp ↑f) s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>s : NonUnitalSubsemiring R<GOAL>↑(NonUnitalSubsemiring.map f s) = ⇑f '' ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>s : NonUnitalSubsemiring R<VAR>y : S<GOAL>y ∈ NonUnitalSubsemiring.map f s ↔ ∃ x ∈ s, f x = y
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<GOAL>NonUnitalSubsemiring.map (NonUnitalRingHom.id R) s = s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>G : Type u_2<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>FunLike G S T<VAR>NonUnitalRingHomClass G S T<VAR>s : NonUnitalSubsemiring R<VAR>g : G<VAR>f : F<GOAL>NonUnitalSubsemiring.map (↑g) (NonUnitalSubsemiring.map (↑f) s) = NonUnitalSubsemiring.map ((↑g).comp ↑f) s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>s : NonUnitalSubsemiring R<VAR>t : NonUnitalSubsemiring S<GOAL>NonUnitalSubsemiring.map f s ≤ t ↔ s ≤ NonUnitalSubsemiring.comap f t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<GOAL>GaloisConnection (NonUnitalSubsemiring.map f) (NonUnitalSubsemiring.comap f)
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s : NonUnitalSubsemiring 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>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<GOAL>↑(NonUnitalRingHom.srange f) = Set.range ⇑f
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>y : S<GOAL>y ∈ NonUnitalRingHom.srange f ↔ ∃ x, f x = y
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<GOAL>NonUnitalRingHom.srange f = NonUnitalSubsemiring.map f ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>x : R<GOAL>f x ∈ NonUnitalRingHom.srange f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring T<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<GOAL>NonUnitalSubsemiring.map g (NonUnitalRingHom.srange f) = NonUnitalRingHom.srange (g.comp f)
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>↑⊥ = {0}
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>x : R<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>p p' : NonUnitalSubsemiring R<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>p p' : NonUnitalSubsemiring R<VAR>x : R<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>S : Set (NonUnitalSubsemiring R)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>S : Set (NonUnitalSubsemiring R)<VAR>x : R<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set (NonUnitalSubsemiring R)<GOAL>(sInf s).toSubsemigroup = ⨅ t ∈ s, t.toSubsemigroup
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set (NonUnitalSubsemiring R)<GOAL>(sInf s).toAddSubmonoid = ⨅ t ∈ s, t.toAddSubmonoid
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>A : NonUnitalSubsemiring R<GOAL>A = ⊤ ↔ ∀ (x : R), x ∈ A
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>↑(NonUnitalSubsemiring.center R) = Set.center R
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>(NonUnitalSubsemiring.center R).toSubsemigroup = Subsemigroup.center R
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>a : R<GOAL>a ∈ Set.center R ↔ AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧ AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧ AddMonoidHom.mul.comp (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulLeft a) ∧ AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>z : R<GOAL>z ∈ NonUnitalSubsemiring.center R ↔ ∀ (g : R), g * z = z * g
<VAR>R : Type u_1<VAR>NonUnitalCommSemiring R<GOAL>NonUnitalSubsemiring.center R = ⊤
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>s : Set R<GOAL>↑(NonUnitalSubsemiring.centralizer s) = s.centralizer
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>s : Set R<GOAL>(NonUnitalSubsemiring.centralizer s).toSubsemigroup = Subsemigroup.centralizer s
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>s : Set R<VAR>z : R<GOAL>z ∈ NonUnitalSubsemiring.centralizer s ↔ ∀ g ∈ s, g * z = z * g
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>s : Set R<GOAL>NonUnitalSubsemiring.center R ≤ NonUnitalSubsemiring.centralizer s
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>s t : Set R<VAR>h : s ⊆ t<GOAL>NonUnitalSubsemiring.centralizer t ≤ NonUnitalSubsemiring.centralizer s
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>s : Set R<GOAL>NonUnitalSubsemiring.centralizer s = ⊤ ↔ s ⊆ ↑(NonUnitalSubsemiring.center R)
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<GOAL>NonUnitalSubsemiring.centralizer Set.univ = NonUnitalSubsemiring.center R
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>x : R<VAR>s : Set R<GOAL>x ∈ NonUnitalSubsemiring.closure s ↔ ∀ (S : NonUnitalSubsemiring R), s ⊆ ↑S → x ∈ S
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<GOAL>s ⊆ ↑(NonUnitalSubsemiring.closure s)
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<VAR>P : R<VAR>hP : P ∉ NonUnitalSubsemiring.closure s<GOAL>P ∉ s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<VAR>t : NonUnitalSubsemiring R<GOAL>NonUnitalSubsemiring.closure s ≤ t ↔ s ⊆ ↑t
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s t : Set R<VAR>h : s ⊆ t<GOAL>NonUnitalSubsemiring.closure s ≤ NonUnitalSubsemiring.closure t
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<VAR>t : NonUnitalSubsemiring R<VAR>h₁ : s ⊆ ↑t<VAR>h₂ : t ≤ NonUnitalSubsemiring.closure s<GOAL>NonUnitalSubsemiring.closure s = t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R ≃+* S<VAR>K : NonUnitalSubsemiring R<VAR>x : S<GOAL>x ∈ NonUnitalSubsemiring.map (↑f) K ↔ f.symm x ∈ K