Documentation

Mathlib.RingTheory.Subsemiring.Basic

Bundled subsemirings #

We define bundled subsemirings and some standard constructions: CompleteLattice structure, Subtype and inclusion ring homomorphisms, subsemiring map, comap and range (rangeS) of a RingHom etc.

class AddSubmonoidWithOneClass (S : Type u_1) (R : Type u_2) [inst : AddMonoidWithOne R] [inst : SetLike S R] extends AddSubmonoidClass , OneMemClass :

    AddSubmonoidWithOneClass S R says S is a type of subsets s ≤ R≤ R that contain 0, 1, and are closed under (+)

    Instances
      theorem natCast_mem {S : Type u_1} {R : Type u_2} [inst : AddMonoidWithOne R] [inst : SetLike S R] (s : S) [inst : AddSubmonoidWithOneClass S R] (n : ) :
      n s
      instance AddSubmonoidWithOneClass.toAddMonoidWithOne {S : Type u_1} {R : Type u_2} [inst : AddMonoidWithOne R] [inst : SetLike S R] (s : S) [inst : AddSubmonoidWithOneClass S R] :
      AddMonoidWithOne { x // x s }
      Equations
      class SubsemiringClass (S : Type u_1) (R : Type u) [inst : NonAssocSemiring R] [inst : SetLike S R] extends SubmonoidClass , AddSubmonoidClass :

        SubsemiringClass S R states that S is a type of subsets s ⊆ R⊆ R that are both a multiplicative and an additive submonoid.

        Instances
          theorem coe_nat_mem {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : SetLike S R] [hSR : SubsemiringClass S R] (s : S) (n : ) :
          n s
          instance SubsemiringClass.toNonAssocSemiring {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : SetLike S R] [hSR : SubsemiringClass S R] (s : S) :
          NonAssocSemiring { x // x s }

          A subsemiring of a NonAssocSemiring inherits a NonAssocSemiring structure

          Equations
          • One or more equations did not get rendered due to their size.
          def SubsemiringClass.subtype {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : SetLike S R] [hSR : SubsemiringClass S R] (s : S) :
          { x // x s } →+* R

          The natural ring hom from a subsemiring of semiring R to R.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem SubsemiringClass.coe_subtype {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : SetLike S R] [hSR : SubsemiringClass S R] (s : S) :
          ↑(SubsemiringClass.subtype s) = Subtype.val
          instance SubsemiringClass.toSemiring {S : Type v} (s : S) {R : Type u_1} [inst : Semiring R] [inst : SetLike S R] [inst : SubsemiringClass S R] :
          Semiring { x // x s }

          A subsemiring of a Semiring is a Semiring.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem SubsemiringClass.coe_pow {S : Type v} (s : S) {R : Type u_1} [inst : Semiring R] [inst : SetLike S R] [inst : SubsemiringClass S R] (x : { x // x s }) (n : ) :
          ↑(x ^ n) = x ^ n
          instance SubsemiringClass.toCommSemiring {S : Type v} (s : S) {R : Type u_1} [inst : CommSemiring R] [inst : SetLike S R] [inst : SubsemiringClass S R] :
          CommSemiring { x // x s }

          A subsemiring of a CommSemiring is a CommSemiring.

          Equations
          • One or more equations did not get rendered due to their size.
          instance SubsemiringClass.toOrderedSemiring {S : Type v} (s : S) {R : Type u_1} [inst : OrderedSemiring R] [inst : SetLike S R] [inst : SubsemiringClass S R] :
          OrderedSemiring { x // x s }

          A subsemiring of an OrderedSemiring is an OrderedSemiring.

          Equations
          • One or more equations did not get rendered due to their size.
          instance SubsemiringClass.toStrictOrderedSemiring {S : Type v} (s : S) {R : Type u_1} [inst : StrictOrderedSemiring R] [inst : SetLike S R] [inst : SubsemiringClass S R] :

          A subsemiring of an StrictOrderedSemiring is an StrictOrderedSemiring.

          Equations
          • One or more equations did not get rendered due to their size.
          instance SubsemiringClass.toOrderedCommSemiring {S : Type v} (s : S) {R : Type u_1} [inst : OrderedCommSemiring R] [inst : SetLike S R] [inst : SubsemiringClass S R] :

          A subsemiring of an OrderedCommSemiring is an OrderedCommSemiring.

          Equations
          • One or more equations did not get rendered due to their size.
          instance SubsemiringClass.toStrictOrderedCommSemiring {S : Type v} (s : S) {R : Type u_1} [inst : StrictOrderedCommSemiring R] [inst : SetLike S R] [inst : SubsemiringClass S R] :

          A subsemiring of an StrictOrderedCommSemiring is an StrictOrderedCommSemiring.

          Equations
          • One or more equations did not get rendered due to their size.
          instance SubsemiringClass.toLinearOrderedSemiring {S : Type v} (s : S) {R : Type u_1} [inst : LinearOrderedSemiring R] [inst : SetLike S R] [inst : SubsemiringClass S R] :

          A subsemiring of a LinearOrderedSemiring is a LinearOrderedSemiring.

          Equations
          • One or more equations did not get rendered due to their size.
          instance SubsemiringClass.toLinearOrderedCommSemiring {S : Type v} (s : S) {R : Type u_1} [inst : LinearOrderedCommSemiring R] [inst : SetLike S R] [inst : SubsemiringClass S R] :

          A subsemiring of a LinearOrderedCommSemiring is a LinearOrderedCommSemiring.

          Equations
          • One or more equations did not get rendered due to their size.
          structure Subsemiring (R : Type u) [inst : NonAssocSemiring R] extends Submonoid :
          • The sum of two elements of an additive subsemigroup belongs to the subsemigroup.

            add_mem' : ∀ {a b : R}, a toSubmonoid.toSubsemigroup.carrierb toSubmonoid.toSubsemigroup.carriera + b toSubmonoid.toSubsemigroup.carrier
          • An additive submonoid contains 0.

            zero_mem' : 0 toSubmonoid.toSubsemigroup.carrier

          A subsemiring of a semiring R is a subset s that is both a multiplicative and an additive submonoid.

          Instances For

            Reinterpret a Subsemiring as an AddSubmonoid.

            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.mem_toSubmonoid {R : Type u} [inst : NonAssocSemiring R] {s : Subsemiring R} {x : R} :
            x s.toSubmonoid x s
            theorem Subsemiring.mem_carrier {R : Type u} [inst : NonAssocSemiring R] {s : Subsemiring R} {x : R} :
            x s.toSubmonoid.toSubsemigroup.carrier x s
            theorem Subsemiring.ext {R : Type u} [inst : NonAssocSemiring R] {S : Subsemiring R} {T : Subsemiring R} (h : ∀ (x : R), x S x T) :
            S = T

            Two subsemirings are equal if they have the same elements.

            def Subsemiring.copy {R : Type u} [inst : NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = S) :

            Copy of a subsemiring with a new carrier equal to the old one. Useful to fix definitional equalities.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.coe_copy {R : Type u} [inst : NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = S) :
            ↑(Subsemiring.copy S s hs) = s
            theorem Subsemiring.copy_eq {R : Type u} [inst : NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = S) :
            theorem Subsemiring.toSubmonoid_injective {R : Type u} [inst : NonAssocSemiring R] :
            Function.Injective Subsemiring.toSubmonoid
            theorem Subsemiring.toSubmonoid_strictMono {R : Type u} [inst : NonAssocSemiring R] :
            StrictMono Subsemiring.toSubmonoid
            theorem Subsemiring.toSubmonoid_mono {R : Type u} [inst : NonAssocSemiring R] :
            Monotone Subsemiring.toSubmonoid
            theorem Subsemiring.toAddSubmonoid_injective {R : Type u} [inst : NonAssocSemiring R] :
            Function.Injective Subsemiring.toAddSubmonoid
            theorem Subsemiring.toAddSubmonoid_strictMono {R : Type u} [inst : NonAssocSemiring R] :
            StrictMono Subsemiring.toAddSubmonoid
            theorem Subsemiring.toAddSubmonoid_mono {R : Type u} [inst : NonAssocSemiring R] :
            Monotone Subsemiring.toAddSubmonoid
            def Subsemiring.mk' {R : Type u} [inst : NonAssocSemiring R] (s : Set R) (sm : Submonoid R) (hm : sm = s) (sa : AddSubmonoid R) (ha : sa = s) :

            Construct a Subsemiring R from a set s, a submonoid sm, and an additive submonoid sa such that x ∈ s ↔ x ∈ sm ↔ x ∈ sa∈ s ↔ x ∈ sm ↔ x ∈ sa↔ x ∈ sm ↔ x ∈ sa∈ sm ↔ x ∈ sa↔ x ∈ sa∈ sa.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.coe_mk' {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : sm = s) {sa : AddSubmonoid R} (ha : sa = s) :
            ↑(Subsemiring.mk' s sm hm sa ha) = s
            @[simp]
            theorem Subsemiring.mem_mk' {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : sm = s) {sa : AddSubmonoid R} (ha : sa = s) {x : R} :
            x Subsemiring.mk' s sm hm sa ha x s
            @[simp]
            theorem Subsemiring.mk'_toSubmonoid {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : sm = s) {sa : AddSubmonoid R} (ha : sa = s) :
            (Subsemiring.mk' s sm hm sa ha).toSubmonoid = sm
            @[simp]
            theorem Subsemiring.mk'_toAddSubmonoid {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : sm = s) {sa : AddSubmonoid R} (ha : sa = s) :
            theorem Subsemiring.one_mem {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) :
            1 s

            A subsemiring contains the semiring's 1.

            theorem Subsemiring.zero_mem {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) :
            0 s

            A subsemiring contains the semiring's 0.

            theorem Subsemiring.mul_mem {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {x : R} {y : R} :
            x sy sx * y s

            A subsemiring is closed under multiplication.

            theorem Subsemiring.add_mem {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {x : R} {y : R} :
            x sy sx + y s

            A subsemiring is closed under addition.

            theorem Subsemiring.list_prod_mem {R : Type u_1} [inst : Semiring R] (s : Subsemiring R) {l : List R} :
            (∀ (x : R), x lx s) → List.prod l s

            Product of a list of elements in a Subsemiring is in the Subsemiring.

            theorem Subsemiring.list_sum_mem {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {l : List R} :
            (∀ (x : R), x lx s) → List.sum l s

            Sum of a list of elements in a Subsemiring is in the Subsemiring.

            theorem Subsemiring.multiset_prod_mem {R : Type u_1} [inst : CommSemiring R] (s : Subsemiring R) (m : Multiset R) :
            (∀ (a : R), a ma s) → Multiset.prod m s

            Product of a multiset of elements in a Subsemiring of a CommSemiring is in the Subsemiring.

            theorem Subsemiring.multiset_sum_mem {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) (m : Multiset R) :
            (∀ (a : R), a ma s) → Multiset.sum m s

            Sum of a multiset of elements in a Subsemiring of a Semiring is in the add_subsemiring.

            theorem Subsemiring.prod_mem {R : Type u_1} [inst : CommSemiring R] (s : Subsemiring R) {ι : Type u_2} {t : Finset ι} {f : ιR} (h : ∀ (c : ι), c tf c s) :
            (Finset.prod t fun i => f i) s

            Product of elements of a subsemiring of a CommSemiring indexed by a Finset is in the subsemiring.

            theorem Subsemiring.sum_mem {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {ι : Type u_1} {t : Finset ι} {f : ιR} (h : ∀ (c : ι), c tf c s) :
            (Finset.sum t fun i => f i) s

            Sum of elements in an Subsemiring of an Semiring indexed by a Finset is in the add_subsemiring.

            @[simp]
            theorem Subsemiring.coe_one {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) :
            1 = 1
            @[simp]
            theorem Subsemiring.coe_zero {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) :
            0 = 0
            @[simp]
            theorem Subsemiring.coe_add {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) (x : { x // x s }) (y : { x // x s }) :
            ↑(x + y) = x + y
            @[simp]
            theorem Subsemiring.coe_mul {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) (x : { x // x s }) (y : { x // x s }) :
            ↑(x * y) = x * y
            theorem Subsemiring.pow_mem {R : Type u_1} [inst : Semiring R] (s : Subsemiring R) {x : R} (hx : x s) (n : ) :
            x ^ n s
            instance Subsemiring.toSemiring {R : Type u_1} [inst : Semiring R] (s : Subsemiring R) :
            Semiring { x // x s }

            A subsemiring of a Semiring is a Semiring.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.coe_pow {R : Type u_1} [inst : Semiring R] (s : Subsemiring R) (x : { x // x s }) (n : ) :
            ↑(x ^ n) = x ^ n
            instance Subsemiring.toCommSemiring {R : Type u_1} [inst : CommSemiring R] (s : Subsemiring R) :
            CommSemiring { x // x s }

            A subsemiring of a CommSemiring is a CommSemiring.

            Equations
            def Subsemiring.subtype {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) :
            { x // x s } →+* R

            The natural ring hom from a subsemiring of semiring R to R.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.coe_subtype {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) :
            ↑(Subsemiring.subtype s) = Subtype.val
            instance Subsemiring.toOrderedSemiring {R : Type u_1} [inst : OrderedSemiring R] (s : Subsemiring R) :
            OrderedSemiring { x // x s }

            A subsemiring of an OrderedSemiring is an OrderedSemiring.

            Equations
            • One or more equations did not get rendered due to their size.

            A subsemiring of a StrictOrderedSemiring is a StrictOrderedSemiring.

            Equations
            • One or more equations did not get rendered due to their size.

            A subsemiring of an OrderedCommSemiring is an OrderedCommSemiring.

            Equations
            • One or more equations did not get rendered due to their size.

            A subsemiring of a StrictOrderedCommSemiring is a StrictOrderedCommSemiring.

            Equations
            • One or more equations did not get rendered due to their size.

            A subsemiring of a LinearOrderedSemiring is a LinearOrderedSemiring.

            Equations
            • One or more equations did not get rendered due to their size.

            A subsemiring of a LinearOrderedCommSemiring is a LinearOrderedCommSemiring.

            Equations
            • One or more equations did not get rendered due to their size.
            theorem Subsemiring.nsmul_mem {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {x : R} (hx : x s) (n : ) :
            n x s
            @[simp]
            theorem Subsemiring.coe_toSubmonoid {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) :
            s.toSubmonoid = s
            @[simp]
            theorem Subsemiring.coe_carrier_toSubmonoid {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) :
            s.toSubmonoid.toSubsemigroup.carrier = s

            The subsemiring R of the semiring R.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.mem_top {R : Type u} [inst : NonAssocSemiring R] (x : R) :
            @[simp]
            theorem Subsemiring.coe_top {R : Type u} [inst : NonAssocSemiring R] :
            = Set.univ
            @[simp]
            theorem Subsemiring.topEquiv_apply {R : Type u} [inst : NonAssocSemiring R] (r : { x // x }) :
            Subsemiring.topEquiv r = r
            @[simp]
            theorem Subsemiring.topEquiv_symm_apply_coe {R : Type u} [inst : NonAssocSemiring R] (r : R) :
            ↑(↑(RingEquiv.symm Subsemiring.topEquiv) r) = r
            def Subsemiring.topEquiv {R : Type u} [inst : NonAssocSemiring R] :
            { x // x } ≃+* R

            The ring equiv between the top element of Subsemiring R and R.

            Equations
            • One or more equations did not get rendered due to their size.
            def Subsemiring.comap {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) (s : Subsemiring S) :

            The preimage of a subsemiring along a ring homomorphism is a subsemiring.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.coe_comap {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (s : Subsemiring S) (f : R →+* S) :
            ↑(Subsemiring.comap f s) = f ⁻¹' s
            @[simp]
            theorem Subsemiring.mem_comap {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {s : Subsemiring S} {f : R →+* S} {x : R} :
            x Subsemiring.comap f s f x s
            theorem Subsemiring.comap_comap {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring T] (s : Subsemiring T) (g : S →+* T) (f : R →+* S) :
            def Subsemiring.map {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) (s : Subsemiring R) :

            The image of a subsemiring along a ring homomorphism is a subsemiring.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.coe_map {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) (s : Subsemiring R) :
            ↑(Subsemiring.map f s) = f '' s
            @[simp]
            theorem Subsemiring.mem_map {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {f : R →+* S} {s : Subsemiring R} {y : S} :
            y Subsemiring.map f s x, x s f x = y
            @[simp]
            theorem Subsemiring.map_id {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) :
            theorem Subsemiring.map_map {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring T] (s : Subsemiring R) (g : S →+* T) (f : R →+* S) :
            noncomputable def Subsemiring.equivMapOfInjective {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (s : Subsemiring R) (f : R →+* S) (hf : Function.Injective f) :
            { x // x s } ≃+* { x // x Subsemiring.map f s }

            A subsemiring is isomorphic to its image under an injective function

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.coe_equivMapOfInjective_apply {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (s : Subsemiring R) (f : R →+* S) (hf : Function.Injective f) (x : { x // x s }) :
            ↑(↑(Subsemiring.equivMapOfInjective s f hf) x) = f x
            def RingHom.rangeS {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) :

            The range of a ring homomorphism is a subsemiring. See Note [range copy pattern].

            Equations
            @[simp]
            theorem RingHom.coe_rangeS {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) :
            @[simp]
            theorem RingHom.mem_rangeS {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {f : R →+* S} {y : S} :
            y RingHom.rangeS f x, f x = y
            theorem RingHom.mem_rangeS_self {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) (x : R) :
            theorem RingHom.map_rangeS {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring T] (g : S →+* T) (f : R →+* S) :
            instance RingHom.fintypeRangeS {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : Fintype R] [inst : DecidableEq S] (f : R →+* S) :

            The range of a morphism of semirings is a fintype, if the domain is a fintype. Note: this instance can form a diamond with Subtype.fintype in the presence of Fintype S.

            Equations
            Equations
            Equations
            • Subsemiring.instInhabitedSubsemiring = { default := }
            theorem Subsemiring.coe_bot {R : Type u} [inst : NonAssocSemiring R] :
            = Set.range Nat.cast
            theorem Subsemiring.mem_bot {R : Type u} [inst : NonAssocSemiring R] {x : R} :
            x n, n = x

            The inf of two subsemirings is their intersection.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.coe_inf {R : Type u} [inst : NonAssocSemiring R] (p : Subsemiring R) (p' : Subsemiring R) :
            ↑(p p') = p p'
            @[simp]
            theorem Subsemiring.mem_inf {R : Type u} [inst : NonAssocSemiring R] {p : Subsemiring R} {p' : Subsemiring R} {x : R} :
            x p p' x p x p'
            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.coe_infₛ {R : Type u} [inst : NonAssocSemiring R] (S : Set (Subsemiring R)) :
            ↑(infₛ S) = Set.interᵢ fun s => Set.interᵢ fun h => s
            theorem Subsemiring.mem_infₛ {R : Type u} [inst : NonAssocSemiring R] {S : Set (Subsemiring R)} {x : R} :
            x infₛ S ∀ (p : Subsemiring R), p Sx p
            @[simp]
            theorem Subsemiring.infₛ_toSubmonoid {R : Type u} [inst : NonAssocSemiring R] (s : Set (Subsemiring R)) :
            (infₛ s).toSubmonoid = t, h, t.toSubmonoid

            Subsemirings of a semiring form a complete lattice.

            Equations
            • One or more equations did not get rendered due to their size.
            theorem Subsemiring.eq_top_iff' {R : Type u} [inst : NonAssocSemiring R] (A : Subsemiring R) :
            A = ∀ (x : R), x A
            def Subsemiring.center (R : Type u_1) [inst : Semiring R] :

            The center of a semiring R is the set of elements that commute with everything in R

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.center_toSubmonoid (R : Type u_1) [inst : Semiring R] :
            theorem Subsemiring.mem_center_iff {R : Type u_1} [inst : Semiring R] {z : R} :
            z Subsemiring.center R ∀ (g : R), g * z = z * g
            instance Subsemiring.decidableMemCenter {R : Type u_1} [inst : Semiring R] [inst : DecidableEq R] [inst : Fintype R] :
            Equations
            instance Subsemiring.commSemiring {R : Type u_1} [inst : Semiring R] :

            The center is commutative.

            Equations
            • One or more equations did not get rendered due to their size.
            def Subsemiring.centralizer {R : Type u_1} [inst : Semiring R] (s : Set R) :

            The centralizer of a set as subsemiring.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Subsemiring.mem_centralizer_iff {R : Type u_1} [inst : Semiring R] {s : Set R} {z : R} :
            z Subsemiring.centralizer s ∀ (g : R), g sg * z = z * g
            def Subsemiring.closure {R : Type u} [inst : NonAssocSemiring R] (s : Set R) :

            The Subsemiring generated by a set.

            Equations
            theorem Subsemiring.mem_closure {R : Type u} [inst : NonAssocSemiring R] {x : R} {s : Set R} :
            x Subsemiring.closure s ∀ (S : Subsemiring R), s Sx S
            @[simp]
            theorem Subsemiring.subset_closure {R : Type u} [inst : NonAssocSemiring R] {s : Set R} :

            The subsemiring generated by a set includes the set.

            @[simp]
            theorem Subsemiring.closure_le {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {t : Subsemiring R} :

            A subsemiring S includes closure s if and only if it includes s.

            theorem Subsemiring.closure_mono {R : Type u} [inst : NonAssocSemiring R] ⦃s : Set R ⦃t : Set R (h : s t) :

            Subsemiring closure of a set is monotone in its argument: if s ⊆ t⊆ t, then closure s ≤ closure t≤ closure t.

            theorem Subsemiring.closure_eq_of_le {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {t : Subsemiring R} (h₁ : s t) (h₂ : t Subsemiring.closure s) :
            theorem Subsemiring.mem_map_equiv {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {f : R ≃+* S} {K : Subsemiring R} {x : S} :
            x Subsemiring.map (f) K ↑(RingEquiv.symm f) x K

            The additive closure of a submonoid is a subsemiring.

            Equations
            • One or more equations did not get rendered due to their size.

            The Subsemiring generated by a multiplicative submonoid coincides with the Subsemiring.closure of the submonoid itself .

            The elements of the subsemiring closure of M are exactly the elements of the additive closure of a multiplicative submonoid M.

            theorem Subsemiring.closure_induction {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {p : RProp} {x : R} (h : x Subsemiring.closure s) (Hs : (x : R) → x sp x) (H0 : p 0) (H1 : p 1) (Hadd : (x y : R) → p xp yp (x + y)) (Hmul : (x y : R) → p xp yp (x * y)) :
            p x

            An induction principle for closure membership. If p holds for 0, 1, and all elements of s, and is preserved under addition and multiplication, then p holds for all elements of the closure of s.

            theorem Subsemiring.closure_induction₂ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {p : RRProp} {x : R} {y : R} (hx : x Subsemiring.closure s) (hy : y Subsemiring.closure s) (Hs : (x : R) → x s(y : R) → y sp x y) (H0_left : (x : R) → p 0 x) (H0_right : (x : R) → p x 0) (H1_left : (x : R) → p 1 x) (H1_right : (x : R) → p x 1) (Hadd_left : (x₁ x₂ y : R) → p x₁ yp x₂ yp (x₁ + x₂) y) (Hadd_right : (x y₁ y₂ : R) → p x y₁p x y₂p x (y₁ + y₂)) (Hmul_left : (x₁ x₂ y : R) → p x₁ yp x₂ yp (x₁ * x₂) y) (Hmul_right : (x y₁ y₂ : R) → p x y₁p x y₂p x (y₁ * y₂)) :
            p x y

            An induction principle for closure membership for predicates with two arguments.

            theorem Subsemiring.mem_closure_iff_exists_list {R : Type u_1} [inst : Semiring R] {s : Set R} {x : R} :
            x Subsemiring.closure s L, (∀ (t : List R), t L∀ (y : R), y ty s) List.sum (List.map List.prod L) = x
            def Subsemiring.gi (R : Type u) [inst : NonAssocSemiring R] :
            GaloisInsertion Subsemiring.closure SetLike.coe

            closure forms a Galois insertion with the coercion to set.

            Equations
            • One or more equations did not get rendered due to their size.

            Closure of a subsemiring S equals S.

            theorem Subsemiring.closure_unionᵢ {R : Type u} [inst : NonAssocSemiring R] {ι : Sort u_1} (s : ιSet R) :
            theorem Subsemiring.map_sup {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (s : Subsemiring R) (t : Subsemiring R) (f : R →+* S) :
            theorem Subsemiring.map_supᵢ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {ι : Sort u_1} (f : R →+* S) (s : ιSubsemiring R) :
            theorem Subsemiring.comap_infᵢ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {ι : Sort u_1} (f : R →+* S) (s : ιSubsemiring S) :
            @[simp]
            theorem Subsemiring.map_bot {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) :
            @[simp]
            theorem Subsemiring.comap_top {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) :
            def Subsemiring.prod {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (s : Subsemiring R) (t : Subsemiring S) :

            Given Subsemirings s, t of semirings R, S respectively, s.prod t is s × t× t as a subsemiring of R × S× S.

            Equations
            • One or more equations did not get rendered due to their size.
            theorem Subsemiring.coe_prod {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (s : Subsemiring R) (t : Subsemiring S) :
            ↑(Subsemiring.prod s t) = s ×ˢ t
            theorem Subsemiring.mem_prod {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {s : Subsemiring R} {t : Subsemiring S} {p : R × S} :
            p Subsemiring.prod s t p.fst s p.snd t
            theorem Subsemiring.prod_mono {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] ⦃s₁ : Subsemiring R ⦃s₂ : Subsemiring R (hs : s₁ s₂) ⦃t₁ : Subsemiring S ⦃t₂ : Subsemiring S (ht : t₁ t₂) :
            theorem Subsemiring.prod_mono_right {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (s : Subsemiring R) :
            theorem Subsemiring.prod_mono_left {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (t : Subsemiring S) :
            def Subsemiring.prodEquiv {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (s : Subsemiring R) (t : Subsemiring S) :
            { x // x Subsemiring.prod s t } ≃+* { x // x s } × { x // x t }

            Product of subsemirings is isomorphic to their product as monoids.

            Equations
            • One or more equations did not get rendered due to their size.
            theorem Subsemiring.mem_supᵢ_of_directed {R : Type u} [inst : NonAssocSemiring R] {ι : Sort u_1} [hι : Nonempty ι] {S : ιSubsemiring R} (hS : Directed (fun x x_1 => x x_1) S) {x : R} :
            (x i, S i) i, x S i
            theorem Subsemiring.coe_supᵢ_of_directed {R : Type u} [inst : NonAssocSemiring R] {ι : Sort u_1} [hι : Nonempty ι] {S : ιSubsemiring R} (hS : Directed (fun x x_1 => x x_1) S) :
            ↑(i, S i) = Set.unionᵢ fun i => ↑(S i)
            theorem Subsemiring.mem_supₛ_of_directedOn {R : Type u} [inst : NonAssocSemiring R] {S : Set (Subsemiring R)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x x_1) S) {x : R} :
            x supₛ S s, s S x s
            theorem Subsemiring.coe_supₛ_of_directedOn {R : Type u} [inst : NonAssocSemiring R] {S : Set (Subsemiring R)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x x_1) S) :
            ↑(supₛ S) = Set.unionᵢ fun s => Set.unionᵢ fun h => s
            def RingHom.domRestrict {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {σR : Type u_1} [inst : SetLike σR R] [inst : SubsemiringClass σR R] (f : R →+* S) (s : σR) :
            { x // x s } →+* S

            Restriction of a ring homomorphism to a subsemiring of the domain.

            Equations
            @[simp]
            theorem RingHom.restrict_apply {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {σR : Type u_1} [inst : SetLike σR R] [inst : SubsemiringClass σR R] (f : R →+* S) {s : σR} (x : { x // x s }) :
            ↑(RingHom.domRestrict f s) x = f x
            def RingHom.codRestrict {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {σS : Type u_1} [inst : SetLike σS S] [inst : SubsemiringClass σS S] (f : R →+* S) (s : σS) (h : ∀ (x : R), f x s) :
            R →+* { x // x s }

            Restriction of a ring homomorphism to a subsemiring of the codomain.

            Equations
            • One or more equations did not get rendered due to their size.
            def RingHom.restrict {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2} [inst : SetLike σR R] [inst : SetLike σS S] [inst : SubsemiringClass σR R] [inst : SubsemiringClass σS S] (f : R →+* S) (s' : σR) (s : σS) (h : ∀ (x : R), x s'f x s) :
            { x // x s' } →+* { x // x s }

            The ring homomorphism from the preimage of s to s.

            Equations
            @[simp]
            theorem RingHom.coe_restrict_apply {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2} [inst : SetLike σR R] [inst : SetLike σS S] [inst : SubsemiringClass σR R] [inst : SubsemiringClass σS S] (f : R →+* S) (s' : σR) (s : σS) (h : ∀ (x : R), x s'f x s) (x : { x // x s' }) :
            ↑(↑(RingHom.restrict f s' s h) x) = f x
            @[simp]
            theorem RingHom.comp_restrict {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2} [inst : SetLike σR R] [inst : SetLike σS S] [inst : SubsemiringClass σR R] [inst : SubsemiringClass σS S] (f : R →+* S) (s' : σR) (s : σS) (h : ∀ (x : R), x s'f x s) :
            def RingHom.rangeSRestrict {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) :
            R →+* { x // x RingHom.rangeS f }

            Restriction of a ring homomorphism to its range interpreted as a subsemiring.

            This is the bundled version of Set.rangeFactorization.

            Equations
            @[simp]
            theorem RingHom.coe_rangeSRestrict {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) (x : R) :
            ↑(↑(RingHom.rangeSRestrict f) x) = f x
            theorem RingHom.rangeS_top_of_surjective {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) (hf : Function.Surjective f) :

            The range of a surjective ring homomorphism is the whole of the codomain.

            def RingHom.eqLocusS {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) (g : R →+* S) :

            The subsemiring of elements x : R such that f x = g x

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem RingHom.eqLocusS_same {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) :
            theorem RingHom.eqOn_sclosure {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {f : R →+* S} {g : R →+* S} {s : Set R} (h : Set.EqOn (f) (g) s) :
            Set.EqOn f g ↑(Subsemiring.closure s)

            If two ring homomorphisms are equal on a set, then they are equal on its subsemiring closure.

            theorem RingHom.eq_of_eqOn_stop {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {f : R →+* S} {g : R →+* S} (h : Set.EqOn f g ) :
            f = g
            theorem RingHom.eq_of_eqOn_sdense {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {s : Set R} (hs : Subsemiring.closure s = ) {f : R →+* S} {g : R →+* S} (h : Set.EqOn (f) (g) s) :
            f = g
            theorem RingHom.map_closureS {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R →+* S) (s : Set R) :

            The image under a ring homomorphism of the subsemiring generated by a set equals the subsemiring generated by the image of the set.

            def Subsemiring.inclusion {R : Type u} [inst : NonAssocSemiring R] {S : Subsemiring R} {T : Subsemiring R} (h : S T) :
            { x // x S } →+* { x // x T }

            The ring homomorphism associated to an inclusion of subsemirings.

            Equations
            @[simp]
            theorem Subsemiring.range_fst {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
            @[simp]
            theorem Subsemiring.range_snd {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
            def RingEquiv.subsemiringCongr {R : Type u} [inst : NonAssocSemiring R] {s : Subsemiring R} {t : Subsemiring R} (h : s = t) :
            { x // x s } ≃+* { x // x t }

            Makes the identity isomorphism from a proof two subsemirings of a multiplicative monoid are equal.

            Equations
            • One or more equations did not get rendered due to their size.
            def RingEquiv.ofLeftInverseS {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {g : SR} {f : R →+* S} (h : Function.LeftInverse g f) :
            R ≃+* { x // x RingHom.rangeS f }

            Restrict a ring homomorphism with a left inverse to a ring isomorphism to its RingHom.rangeS.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem RingEquiv.ofLeftInverseS_apply {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {g : SR} {f : R →+* S} (h : Function.LeftInverse g f) (x : R) :
            ↑(↑(RingEquiv.ofLeftInverseS h) x) = f x
            @[simp]
            theorem RingEquiv.ofLeftInverseS_symm_apply {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {g : SR} {f : R →+* S} (h : Function.LeftInverse g f) (x : { x // x RingHom.rangeS f }) :
            @[simp]
            theorem RingEquiv.subsemiringMap_apply_coe {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) (s : Subsemiring R) :
            ∀ (a : ↑(Subsemiring.toAddSubmonoid s)), ↑(↑(RingEquiv.subsemiringMap e s) a) = e a
            @[simp]
            theorem RingEquiv.subsemiringMap_symm_apply_coe {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) (s : Subsemiring R) :
            ∀ (a : ↑(↑(RingEquiv.toAddEquiv e) '' ↑(Subsemiring.toAddSubmonoid s))), ↑(↑(RingEquiv.symm (RingEquiv.subsemiringMap e s)) a) = ↑(AddEquiv.symm e) a
            def RingEquiv.subsemiringMap {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) (s : Subsemiring R) :
            { x // x s } ≃+* { x // x Subsemiring.map (RingEquiv.toRingHom e) s }

            Given an equivalence e : R ≃+* S≃+* S of semirings and a subsemiring s of R, subsemiring_map e s is the induced equivalence between s and s.map e

            Equations
            • One or more equations did not get rendered due to their size.

            Actions by Subsemirings #

            These are just copies of the definitions about Submonoid starting from submonoid.mul_action. The only new result is subsemiring.module.

            When R is commutative, algebra.of_subsemiring provides a stronger result than those found in this file, which uses the same scalar action.

            instance Subsemiring.smul {R' : Type u_1} {α : Type u_2} [inst : NonAssocSemiring R'] [inst : SMul R' α] (S : Subsemiring R') :
            SMul { x // x S } α

            The action by a subsemiring is the action by the underlying semiring.

            Equations
            theorem Subsemiring.smul_def {R' : Type u_1} {α : Type u_2} [inst : NonAssocSemiring R'] [inst : SMul R' α] {S : Subsemiring R'} (g : { x // x S }) (m : α) :
            g m = g m
            instance Subsemiring.smulCommClass_left {R' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring R'] [inst : SMul R' β] [inst : SMul α β] [inst : SMulCommClass R' α β] (S : Subsemiring R') :
            SMulCommClass { x // x S } α β
            Equations
            instance Subsemiring.smulCommClass_right {R' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring R'] [inst : SMul α β] [inst : SMul R' β] [inst : SMulCommClass α R' β] (S : Subsemiring R') :
            SMulCommClass α { x // x S } β
            Equations
            instance Subsemiring.isScalarTower {R' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring R'] [inst : SMul α β] [inst : SMul R' α] [inst : SMul R' β] [inst : IsScalarTower R' α β] (S : Subsemiring R') :
            IsScalarTower { x // x S } α β

            Note that this provides IsScalarTower S R R which is needed by smul_mul_assoc.

            Equations
            instance Subsemiring.faithfulSMul {R' : Type u_1} {α : Type u_2} [inst : NonAssocSemiring R'] [inst : SMul R' α] [inst : FaithfulSMul R' α] (S : Subsemiring R') :
            FaithfulSMul { x // x S } α
            Equations

            The action by a subsemiring is the action by the underlying semiring.

            Equations
            • One or more equations did not get rendered due to their size.
            instance Subsemiring.mulAction {R' : Type u_1} {α : Type u_2} [inst : Semiring R'] [inst : MulAction R' α] (S : Subsemiring R') :
            MulAction { x // x S } α

            The action by a subsemiring is the action by the underlying semiring.

            Equations
            instance Subsemiring.distribMulAction {R' : Type u_1} {α : Type u_2} [inst : Semiring R'] [inst : AddMonoid α] [inst : DistribMulAction R' α] (S : Subsemiring R') :
            DistribMulAction { x // x S } α

            The action by a subsemiring is the action by the underlying semiring.

            Equations
            instance Subsemiring.mulDistribMulAction {R' : Type u_1} {α : Type u_2} [inst : Semiring R'] [inst : Monoid α] [inst : MulDistribMulAction R' α] (S : Subsemiring R') :
            MulDistribMulAction { x // x S } α

            The action by a subsemiring is the action by the underlying semiring.

            Equations
            instance Subsemiring.mulActionWithZero {R' : Type u_1} {α : Type u_2} [inst : Semiring R'] [inst : Zero α] [inst : MulActionWithZero R' α] (S : Subsemiring R') :
            MulActionWithZero { x // x S } α

            The action by a subsemiring is the action by the underlying semiring.

            Equations
            instance Subsemiring.module {R' : Type u_1} {α : Type u_2} [inst : Semiring R'] [inst : AddCommMonoid α] [inst : Module R' α] (S : Subsemiring R') :
            Module { x // x S } α

            The action by a subsemiring is the action by the underlying semiring.

            Equations

            The action by a subsemiring is the action by the underlying semiring.

            Equations
            • One or more equations did not get rendered due to their size.
            instance Subsemiring.center.smulCommClass_left {R' : Type u_1} [inst : Semiring R'] :

            The center of a semiring acts commutatively on that semiring.

            Equations
            instance Subsemiring.center.smulCommClass_right {R' : Type u_1} [inst : Semiring R'] :

            The center of a semiring acts commutatively on that semiring.

            Equations
            def Subsemiring.closureCommSemiringOfComm {R' : Type u_1} [inst : Semiring R'] {s : Set R'} (hcomm : ∀ (a : R'), a s∀ (b : R'), b sa * b = b * a) :

            If all the elements of a set s commute, then closure s is a commutative monoid.

            Equations
            def posSubmonoid (R : Type u_1) [inst : StrictOrderedSemiring R] :

            Submonoid of positive elements of an ordered semiring.

            Equations
            • posSubmonoid R = { toSubsemigroup := { carrier := { x | 0 < x }, mul_mem' := (_ : ∀ {x y : R}, 0 < x0 < y0 < x * y) }, one_mem' := (_ : 0 < 1) }
            @[simp]
            theorem mem_posSubmonoid {R : Type u_1} [inst : StrictOrderedSemiring R] (u : Rˣ) :
            u posSubmonoid R 0 < u