ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Module R A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>Algebra R S<VAR>a : A<VAR>f : S → R<VAR>IsScalarTower R S A<VAR>h : QuasispectrumRestricts a f<GOAL>quasispectrum S a ⊆ f ⁻¹' quasispectrum R a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Module R A<VAR>Module S A<VAR>Algebra R S<VAR>a b : A<VAR>f : S → R<VAR>ha : QuasispectrumRestricts a f<VAR>h : quasispectrum S a = quasispectrum S b<GOAL>QuasispectrumRestricts b f
<VAR>R₁ : Type u_6<VAR>R₂ : Type u_7<VAR>R₃ : Type u_8<VAR>A : Type u_9<VAR>Semifield R₁<VAR>Field R₂<VAR>Field R₃<VAR>NonUnitalRing A<VAR>Module R₁ A<VAR>Module R₂ A<VAR>Module R₃ A<VAR>Algebra R₁ R₂<VAR>Algebra R₂ R₃<VAR>Algebra R₁ R₃<VAR>IsScalarTower R₁ R₂ R₃<VAR>IsScalarTower R₂ R₃ A<VAR>IsScalarTower R₃ A A<VAR>SMulCommClass R₃ A A<VAR>a : A<VAR>f : R₃ → R₂<VAR>g : R₂ → R₁<VAR>e : R₃ → R₁<VAR>hfge : g ∘ f = e<VAR>hf : QuasispectrumRestricts a f<VAR>hg : QuasispectrumRestricts a g<GOAL>QuasispectrumRestricts a e
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>a : A<VAR>f : S → R<VAR>h : SpectrumRestricts a f<GOAL>Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>a : A<VAR>f : S → R<VAR>h₁ : Function.LeftInverse f ⇑(algebraMap R S)<VAR>h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)<GOAL>SpectrumRestricts a f
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>a : A<VAR>f : S → R<GOAL>SpectrumRestricts a f ↔ Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a) ∧ Function.LeftInverse f ⇑(algebraMap R S)
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>a : A<VAR>f : S → R<VAR>hf : Function.LeftInverse f ⇑(algebraMap R S)<VAR>h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)<GOAL>SpectrumRestricts a f
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>a : A<VAR>f : S → R<VAR>IsScalarTower R S A<VAR>h : SpectrumRestricts a f<GOAL>⇑(algebraMap R S) '' spectrum R a = spectrum S a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>a : A<VAR>f : S → R<VAR>IsScalarTower R S A<VAR>h : SpectrumRestricts a f<GOAL>f '' spectrum S a = spectrum R a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>a : A<VAR>f : S → R<VAR>IsScalarTower R S A<VAR>h : SpectrumRestricts a f<VAR>s : S<VAR>hs : s ∈ spectrum S a<GOAL>f s ∈ spectrum R a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>a : A<VAR>f : S → R<VAR>IsScalarTower R S A<VAR>h : SpectrumRestricts a f<GOAL>spectrum S a ⊆ f ⁻¹' spectrum R a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>a b : A<VAR>f : S → R<VAR>ha : SpectrumRestricts a f<VAR>h : spectrum S a = spectrum S b<GOAL>SpectrumRestricts b f
<VAR>S : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Algebra R S<VAR>Module R A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>IsScalarTower R S A<VAR>a : A<VAR>f : S → R<GOAL>QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>a : A<VAR>f : S → R<GOAL>QuasispectrumRestricts a f ↔ SpectrumRestricts a f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>Mul A<VAR>f g : MonoidAlgebra R A<VAR>a0 b0 : A<VAR>h : UniqueMul f.support g.support a0 b0<GOAL>(f * g) (a0 * b0) = f a0 * g b0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>Add A<VAR>f g : AddMonoidAlgebra R A<VAR>a0 b0 : A<VAR>h : UniqueAdd f.support g.support a0 b0<GOAL>(f * g) (a0 + b0) = f a0 * g b0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>DecidableEq G<VAR>a b : MonoidAlgebra k G<GOAL>(a * b).support ⊆ a.support * b.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>DecidableEq G<VAR>Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>a : G<GOAL>(MonoidAlgebra.single a r * f).support ⊆ Finset.image (fun x => a * x) f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>DecidableEq G<VAR>Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>a : G<GOAL>(f * MonoidAlgebra.single a r).support ⊆ Finset.image (fun x => x * a) f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>DecidableEq G<VAR>Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), r * y = 0 ↔ y = 0<VAR>x : G<VAR>lx : IsLeftRegular x<GOAL>(MonoidAlgebra.single x r * f).support = Finset.image (fun x_1 => x * x_1) f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>DecidableEq G<VAR>Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), y * r = 0 ↔ y = 0<VAR>x : G<VAR>rx : IsRightRegular x<GOAL>(f * MonoidAlgebra.single x r).support = Finset.image (fun x_1 => x_1 * x) f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>IsRightCancelMul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), y * r = 0 ↔ y = 0<VAR>x : G<GOAL>(f * MonoidAlgebra.single x r).support = Finset.map (mulRightEmbedding x) f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>IsLeftCancelMul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), r * y = 0 ↔ y = 0<VAR>x : G<GOAL>(MonoidAlgebra.single x r * f).support = Finset.map (mulLeftEmbedding x) f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>One G<GOAL>Finsupp.support 1 ⊆ 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>One G<VAR>NeZero 1<GOAL>Finsupp.support 1 = 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<VAR>f : MonoidAlgebra k G<GOAL>f ∈ Submodule.span k (⇑(MonoidAlgebra.of k G) '' ↑f.support)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>DecidableEq G<VAR>Add G<VAR>a b : AddMonoidAlgebra k G<GOAL>(a * b).support ⊆ a.support + b.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>IsRightCancelAdd G<VAR>f : AddMonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), y * r = 0 ↔ y = 0<VAR>x : G<GOAL>(f * AddMonoidAlgebra.single x r).support = Finset.map (addRightEmbedding x) f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>IsLeftCancelAdd G<VAR>f : AddMonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), r * y = 0 ↔ y = 0<VAR>x : G<GOAL>(AddMonoidAlgebra.single x r * f).support = Finset.map (addLeftEmbedding x) f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Zero G<GOAL>Finsupp.support 1 ⊆ 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Zero G<VAR>NeZero 1<GOAL>Finsupp.support 1 = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddZeroClass G<VAR>f : AddMonoidAlgebra k G<GOAL>f ∈ Submodule.span k (⇑(AddMonoidAlgebra.of k G) '' ↑f.support)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>f : AddMonoidAlgebra k G<GOAL>f ∈ Submodule.span k (AddMonoidAlgebra.of' k G '' ↑f.support)
<VAR>k : Type u_1<VAR>G : Type u_3<VAR>Monoid G<VAR>Semiring k<VAR>s : Set G<VAR>x : MonoidAlgebra k G<GOAL>x ∈ Ideal.span (⇑(MonoidAlgebra.of k G) '' s) ↔ ∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = d * m'
<VAR>k : Type u_1<VAR>A : Type u_2<VAR>AddMonoid A<VAR>Semiring k<VAR>s : Set A<VAR>x : AddMonoidAlgebra k A<GOAL>x ∈ Ideal.span (AddMonoidAlgebra.of' k A '' s) ↔ ∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = d + m'
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>SetLike S R<VAR>hSR : SubringClass S R<VAR>s : S<VAR>n : ℤ<GOAL>↑n ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>SetLike S R<VAR>hSR : SubringClass S R<VAR>s : S<GOAL>⇑(SubringClass.subtype s) = Subtype.val
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>SetLike S R<VAR>hSR : SubringClass S R<VAR>s : S<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>SetLike S R<VAR>hSR : SubringClass S R<VAR>s : S<VAR>n : ℤ<GOAL>↑↑n = ↑n
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x : R<GOAL>x ∈ s.toSubsemiring ↔ x ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x : R<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>S : Subsemiring R<VAR>x : R<VAR>h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier<GOAL>x ∈ { toSubsemiring := S, neg_mem' := h } ↔ x ∈ S
<VAR>R : Type u<VAR>Ring R<VAR>S : Subsemiring R<VAR>h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier<GOAL>↑{ toSubsemiring := S, neg_mem' := h } = ↑S
<VAR>R : Type u<VAR>Ring R<VAR>S S' : Subsemiring R<VAR>h₁ : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier<VAR>h₂ : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier<GOAL>{ toSubsemiring := S, neg_mem' := h₁ } ≤ { toSubsemiring := S', neg_mem' := h₂ } ↔ S ≤ S'
<VAR>R : Type u<VAR>Ring R<VAR>S T : Subring R<VAR>h : ∀ (x : R), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>R : Type u<VAR>Ring R<VAR>S : Subring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type u<VAR>Ring R<VAR>S : Subring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>R : Type u<VAR>Ring R<GOAL>Function.Injective Subring.toSubsemiring
<VAR>R : Type u<VAR>Ring R<GOAL>StrictMono Subring.toSubsemiring
<VAR>R : Type u<VAR>Ring R<GOAL>Monotone Subring.toSubsemiring
<VAR>R : Type u<VAR>Ring R<GOAL>Function.Injective Subring.toAddSubgroup
<VAR>R : Type u<VAR>Ring R<GOAL>StrictMono Subring.toAddSubgroup
<VAR>R : Type u<VAR>Ring R<GOAL>Monotone Subring.toAddSubgroup
<VAR>R : Type u<VAR>Ring R<GOAL>Function.Injective fun s => s.toSubmonoid
<VAR>R : Type u<VAR>Ring R<GOAL>StrictMono fun s => s.toSubmonoid
<VAR>R : Type u<VAR>Ring R<GOAL>Monotone fun s => s.toSubmonoid
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>sm : Submonoid R<VAR>hm : ↑sm = s<VAR>sa : AddSubgroup R<VAR>ha : ↑sa = s<GOAL>↑(Subring.mk' s sm sa hm ha) = s
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>sm : Submonoid R<VAR>hm : ↑sm = s<VAR>sa : AddSubgroup R<VAR>ha : ↑sa = s<VAR>x : R<GOAL>x ∈ Subring.mk' s sm sa hm ha ↔ x ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>sm : Submonoid R<VAR>hm : ↑sm = s<VAR>sa : AddSubgroup R<VAR>ha : ↑sa = s<GOAL>(Subring.mk' s sm sa hm ha).toSubmonoid = sm
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>sm : Submonoid R<VAR>hm : ↑sm = s<VAR>sa : AddSubgroup R<VAR>ha : ↑sa = s<GOAL>(Subring.mk' s sm sa hm ha).toAddSubgroup = sa
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>1 ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>0 ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x y : R<GOAL>x ∈ s → y ∈ s → x * y ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x y : R<GOAL>x ∈ s → y ∈ s → x + y ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x : R<GOAL>x ∈ s → -x ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x y : R<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x - y ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>l : List R<GOAL>(∀ x ∈ l, x ∈ s) → l.prod ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>l : List R<GOAL>(∀ x ∈ l, x ∈ s) → l.sum ∈ s
<VAR>R : Type u_1<VAR>CommRing R<VAR>s : Subring R<VAR>m : Multiset R<GOAL>(∀ a ∈ m, a ∈ s) → m.prod ∈ s
<VAR>R : Type u_1<VAR>Ring R<VAR>s : Subring R<VAR>m : Multiset R<GOAL>(∀ a ∈ m, a ∈ s) → m.sum ∈ s
<VAR>R : Type u_1<VAR>CommRing R<VAR>s : Subring 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_1<VAR>Ring R<VAR>s : Subring 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>Ring R<VAR>s : Subring R<VAR>x : R<VAR>hx : x ∈ s<VAR>n : ℤ<GOAL>n • x ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x : R<VAR>hx : x ∈ s<VAR>n : ℕ<GOAL>x ^ n ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x y : ↥s<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x : ↥s<GOAL>↑(-x) = -↑x
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x y : ↥s<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>↑0 = 0
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>↑1 = 1
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x : ↥s<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x : ↥s<GOAL>↑x = 0 ↔ x = 0
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>⇑s.subtype = Subtype.val
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>n : ℤ<GOAL>↑↑n = ↑n
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>↑s.toSubsemiring = ↑s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x : R<GOAL>x ∈ s.toSubmonoid ↔ x ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>↑s.toSubmonoid = ↑s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<VAR>x : R<GOAL>x ∈ s.toAddSubgroup ↔ x ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>↑s.toAddSubgroup = ↑s
<VAR>R : Type u<VAR>Ring R<VAR>x : R<GOAL>x ∈ ⊤
<VAR>R : Type u<VAR>Ring R<GOAL>↑⊤ = Set.univ
<VAR>R : Type u<VAR>Ring R<VAR>r : ↥⊤<GOAL>Subring.topEquiv r = ↑r
<VAR>R : Type u<VAR>Ring R<VAR>r : R<GOAL>↑(Subring.topEquiv.symm r) = r
<VAR>R : Type u_1<VAR>Ring R<VAR>Fintype R<GOAL>Fintype.card ↥⊤ = Fintype.card R
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring S<VAR>f : R →+* S<GOAL>↑(Subring.comap f s) = ⇑f ⁻¹' ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring S<VAR>f : R →+* S<VAR>x : R<GOAL>x ∈ Subring.comap f s ↔ f x ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>Ring R<VAR>Ring S<VAR>Ring T<VAR>s : Subring T<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>Subring.comap f (Subring.comap g s) = Subring.comap (g.comp f) s
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>s : Subring R<GOAL>↑(Subring.map f s) = ⇑f '' ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>s : Subring R<VAR>y : S<GOAL>y ∈ Subring.map f s ↔ ∃ x ∈ s, f x = y
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>Subring.map (RingHom.id R) s = s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>Ring R<VAR>Ring S<VAR>Ring T<VAR>s : Subring R<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>Subring.map g (Subring.map f s) = Subring.map (g.comp f) s
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>s : Subring R<VAR>t : Subring S<GOAL>Subring.map f s ≤ t ↔ s ≤ Subring.comap f t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>GaloisConnection (Subring.map f) (Subring.comap f)
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring R<VAR>f : R →+* S<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>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>↑f.range = Set.range ⇑f
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring 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>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>f.range = Subring.map f ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>x : R<GOAL>f x ∈ f.range
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>Ring R<VAR>Ring S<VAR>Ring T<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>Subring.map g f.range = (g.comp f).range
<VAR>R : Type u<VAR>Ring R<GOAL>↑⊥ = Set.range Int.cast
<VAR>R : Type u<VAR>Ring R<VAR>x : R<GOAL>x ∈ ⊥ ↔ ∃ n, ↑n = x
<VAR>R : Type u<VAR>Ring R<VAR>p p' : Subring R<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>R : Type u<VAR>Ring R<VAR>p p' : Subring R<VAR>x : R<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>R : Type u<VAR>Ring R<VAR>S : Set (Subring R)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>Ring R<VAR>S : Set (Subring R)<VAR>x : R<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>R : Type u<VAR>Ring R<VAR>ι : Sort u_1<VAR>S : ι → Subring R<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Sort u_1<VAR>S : ι → Subring R<VAR>x : R<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>R : Type u<VAR>Ring R<VAR>s : Set (Subring R)<GOAL>(sInf s).toSubmonoid = ⨅ t ∈ s, t.toSubmonoid
<VAR>R : Type u<VAR>Ring R<VAR>s : Set (Subring R)<GOAL>(sInf s).toAddSubgroup = ⨅ t ∈ s, t.toAddSubgroup
<VAR>R : Type u<VAR>Ring R<VAR>A : Subring R<GOAL>A = ⊤ ↔ ∀ (x : R), x ∈ A
<VAR>R : Type u<VAR>Ring R<GOAL>↑(Subring.center R) = Set.center R
<VAR>R : Type u<VAR>Ring R<GOAL>(Subring.center R).toSubsemiring = Subsemiring.center R
<VAR>R : Type u<VAR>Ring R<VAR>z : R<GOAL>z ∈ Subring.center R ↔ ∀ (g : R), g * z = z * g
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Subring.center R = ⊤
<VAR>K : Type u<VAR>DivisionRing K<VAR>a : ↥(Subring.center K)<GOAL>↑a⁻¹ = (↑a)⁻¹
<VAR>K : Type u<VAR>DivisionRing K<VAR>a b : ↥(Subring.center K)<GOAL>↑(a / b) = ↑a / ↑b
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<GOAL>↑(Subring.centralizer s) = s.centralizer
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<GOAL>(Subring.centralizer s).toSubmonoid = Submonoid.centralizer s
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<GOAL>(Subring.centralizer s).toSubsemiring = Subsemiring.centralizer s
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>z : R<GOAL>z ∈ Subring.centralizer s ↔ ∀ g ∈ s, g * z = z * g
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<GOAL>Subring.center R ≤ Subring.centralizer s
<VAR>R : Type u<VAR>Ring R<VAR>s t : Set R<VAR>h : s ⊆ t<GOAL>Subring.centralizer t ≤ Subring.centralizer s
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<GOAL>Subring.centralizer s = ⊤ ↔ s ⊆ ↑(Subring.center R)
<VAR>R : Type u<VAR>Ring R<GOAL>Subring.centralizer Set.univ = Subring.center R
<VAR>R : Type u<VAR>Ring R<VAR>x : R<VAR>s : Set R<GOAL>x ∈ Subring.closure s ↔ ∀ (S : Subring R), s ⊆ ↑S → x ∈ S
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<GOAL>s ⊆ ↑(Subring.closure s)
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>P : R<VAR>hP : P ∉ Subring.closure s<GOAL>P ∉ s
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>t : Subring R<GOAL>Subring.closure s ≤ t ↔ s ⊆ ↑t
<VAR>R : Type u<VAR>Ring R<VAR>s t : Set R<VAR>h : s ⊆ t<GOAL>Subring.closure s ≤ Subring.closure t
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>t : Subring R<VAR>h₁ : s ⊆ ↑t<VAR>h₂ : t ≤ Subring.closure s<GOAL>Subring.closure s = t
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>p : R → Prop<VAR>x : R<VAR>h : x ∈ Subring.closure s<VAR>Hs : ∀ x ∈ s, p x<VAR>zero : p 0<VAR>one : p 1<VAR>add : ∀ (x y : R), p x → p y → p (x + y)<VAR>neg : ∀ (x : R), p x → p (-x)<VAR>mul : ∀ (x y : R), p x → p y → p (x * y)<GOAL>p x
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>p : (x : R) → x ∈ Subring.closure s → Prop<VAR>mem : ∀ (x : R) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>one : p 1 ⋯<VAR>add : ∀ (x : R) (hx : x ∈ Subring.closure s) (y : R) (hy : y ∈ Subring.closure s), p x hx → p y hy → p (x + y) ⋯<VAR>neg : ∀ (x : R) (hx : x ∈ Subring.closure s), p x hx → p (-x) ⋯<VAR>mul : ∀ (x : R) (hx : x ∈ Subring.closure s) (y : R) (hy : y ∈ Subring.closure s), p x hx → p y hy → p (x * y) ⋯<VAR>a : R<VAR>ha : a ∈ Subring.closure s<GOAL>p a ha
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>p : R → R → Prop<VAR>a b : R<VAR>ha : a ∈ Subring.closure s<VAR>hb : b ∈ Subring.closure s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>H0_left : ∀ (x : R), p 0 x<VAR>H0_right : ∀ (x : R), p x 0<VAR>H1_left : ∀ (x : R), p 1 x<VAR>H1_right : ∀ (x : R), p x 1<VAR>Hneg_left : ∀ (x y : R), p x y → p (-x) y<VAR>Hneg_right : ∀ (x y : R), p x y → p x (-y)<VAR>Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)<GOAL>p a b
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>x : R<GOAL>x ∈ Subring.closure s ↔ x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>x : R<VAR>h : x ∈ Subring.closure s<GOAL>∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>Subring.closure ↑s = s
<VAR>R : Type u<VAR>Ring R<GOAL>Subring.closure ∅ = ⊥
<VAR>R : Type u<VAR>Ring R<GOAL>Subring.closure Set.univ = ⊤
<VAR>R : Type u<VAR>Ring R<VAR>s t : Set R<GOAL>Subring.closure (s ∪ t) = Subring.closure s ⊔ Subring.closure t
<VAR>R : Type u<VAR>Ring R<VAR>ι : Sort u_1<VAR>s : ι → Set R<GOAL>Subring.closure (⋃ i, s i) = ⨆ i, Subring.closure (s i)
<VAR>R : Type u<VAR>Ring R<VAR>s : Set (Set R)<GOAL>Subring.closure (⋃₀ s) = ⨆ t ∈ s, Subring.closure t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s t : Subring R<VAR>f : R →+* S<GOAL>Subring.map f (s ⊔ t) = Subring.map f s ⊔ Subring.map f t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>ι : Sort u_1<VAR>f : R →+* S<VAR>s : ι → Subring R<GOAL>Subring.map f (iSup s) = ⨆ i, Subring.map f (s i)
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s t : Subring S<VAR>f : R →+* S<GOAL>Subring.comap f (s ⊓ t) = Subring.comap f s ⊓ Subring.comap f t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>ι : Sort u_1<VAR>f : R →+* S<VAR>s : ι → Subring S<GOAL>Subring.comap f (iInf s) = ⨅ i, Subring.comap f (s i)
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>Subring.map f ⊥ = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>Subring.comap f ⊤ = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring R<VAR>t : Subring S<GOAL>↑(s.prod t) = ↑s ×ˢ ↑t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring R<VAR>t : Subring S<VAR>p : R × S<GOAL>p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s₁ s₂ : Subring R<VAR>hs : s₁ ≤ s₂<VAR>t₁ t₂ : Subring S<VAR>ht : t₁ ≤ t₂<GOAL>s₁.prod t₁ ≤ s₂.prod t₂
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring R<GOAL>Monotone fun t => s.prod t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>t : Subring S<GOAL>Monotone fun s => s.prod t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring R<GOAL>s.prod ⊤ = Subring.comap (RingHom.fst R S) s
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring S<GOAL>⊤.prod s = Subring.comap (RingHom.snd R S) s
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<GOAL>⊤.prod ⊤ = ⊤
<VAR>R : Type u<VAR>Ring R<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>R : Type u<VAR>Ring R<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>R : Type u<VAR>Ring R<VAR>S : Set (Subring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>R : Type u<VAR>Ring R<VAR>S : Set (Subring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<GOAL>↑(sSup S) = ⋃ s ∈ S, ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R ≃+* S<VAR>K : Subring R<VAR>x : S<GOAL>x ∈ Subring.map (↑f) K ↔ f.symm x ∈ K
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R ≃+* S<VAR>K : Subring R<GOAL>Subring.map (↑f) K = Subring.comap (↑f.symm) K
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R ≃+* S<VAR>K : Subring S<GOAL>Subring.comap (↑f) K = Subring.map (↑f.symm) K
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>x : R<GOAL>↑(f.rangeRestrict x) = f x
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>Function.Surjective ⇑f.rangeRestrict
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>f.range = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>f.range = ⊤
<VAR>R : Type u<VAR>Ring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<GOAL>f.eqLocus f = ⊤
<VAR>R : Type u<VAR>Ring R<VAR>S : Type v<VAR>Semiring S<VAR>f g : R →+* S<VAR>s : Set R<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(Subring.closure s)
<VAR>R : Type u<VAR>Ring R<VAR>S : Type v<VAR>Semiring S<VAR>f g : R →+* S<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g