Documentation

Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Bundled non-unital subsemirings #

We define bundled non-unital subsemirings and some standard constructions: subtype and inclusion ring homomorphisms.

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

Instances
    @[instance 75]

    A non-unital subsemiring of a NonUnitalNonAssocSemiring inherits a NonUnitalNonAssocSemiring structure

    Equations

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

      Equations
        Instances For
          @[simp]
          theorem NonUnitalSubsemiringClass.subtype_apply {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] {s : S} (x : s) :
          (subtype s) x = x
          @[deprecated NonUnitalSubsemiringClass.coe_subtype (since := "2025-02-18")]

          Alias of NonUnitalSubsemiringClass.coe_subtype.

          A non-unital subsemiring of a NonUnitalSemiring is a NonUnitalSemiring.

          Equations

            Note: currently, there are no ordered versions of non-unital rings.

            A non-unital subsemiring of a non-unital semiring R is a subset s that is both an additive submonoid and a semigroup.

            Instances For

              The actual NonUnitalSubsemiring obtained from an element of a NonUnitalSubsemiringClass.

              Equations
                Instances For
                  @[simp]
                  @[instance 100]
                  instance NonUnitalSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul {R : Type u} [NonUnitalNonAssocSemiring R] :
                  CanLift (Set R) (NonUnitalSubsemiring R) SetLike.coe fun (s : Set R) => 0 s (∀ {x y : R}, x sy sx + y s) ∀ {x y : R}, x sy sx * y s
                  theorem NonUnitalSubsemiring.ext {R : Type u} [NonUnitalNonAssocSemiring R] {S T : NonUnitalSubsemiring R} (h : ∀ (x : R), x S x T) :
                  S = T

                  Two non-unital subsemirings are equal if they have the same elements.

                  theorem NonUnitalSubsemiring.ext_iff {R : Type u} [NonUnitalNonAssocSemiring R] {S T : NonUnitalSubsemiring R} :
                  S = T ∀ (x : R), x S x T

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

                  Equations
                    Instances For
                      @[simp]
                      theorem NonUnitalSubsemiring.coe_copy {R : Type u} [NonUnitalNonAssocSemiring R] (S : NonUnitalSubsemiring R) (s : Set R) (hs : s = S) :
                      (S.copy s hs) = s
                      theorem NonUnitalSubsemiring.copy_eq {R : Type u} [NonUnitalNonAssocSemiring R] (S : NonUnitalSubsemiring R) (s : Set R) (hs : s = S) :
                      S.copy s hs = S
                      def NonUnitalSubsemiring.mk' {R : Type u} [NonUnitalNonAssocSemiring R] (s : Set R) (sg : Subsemigroup R) (hg : sg = s) (sa : AddSubmonoid R) (ha : sa = s) :

                      Construct a NonUnitalSubsemiring R from a set s, a subsemigroup sg, and an additive submonoid sa such that x ∈ s ↔ x ∈ sg ↔ x ∈ sa.

                      Equations
                        Instances For
                          @[simp]
                          theorem NonUnitalSubsemiring.coe_mk' {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : sg = s) {sa : AddSubmonoid R} (ha : sa = s) :
                          (NonUnitalSubsemiring.mk' s sg hg sa ha) = s
                          @[simp]
                          theorem NonUnitalSubsemiring.mem_mk' {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : sg = s) {sa : AddSubmonoid R} (ha : sa = s) {x : R} :
                          x NonUnitalSubsemiring.mk' s sg hg sa ha x s
                          @[simp]
                          theorem NonUnitalSubsemiring.mk'_toSubsemigroup {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : sg = s) {sa : AddSubmonoid R} (ha : sa = s) :
                          @[simp]
                          theorem NonUnitalSubsemiring.mk'_toAddSubmonoid {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : sg = s) {sa : AddSubmonoid R} (ha : sa = s) :
                          @[simp]
                          theorem NonUnitalSubsemiring.coe_add {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) (x y : s) :
                          ↑(x + y) = x + y
                          @[simp]
                          theorem NonUnitalSubsemiring.coe_mul {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) (x y : s) :
                          ↑(x * y) = x * y

                          Note: currently, there are no ordered versions of non-unital rings.

                          The non-unital subsemiring R of the non-unital semiring R.

                          Equations

                            The inf of two non-unital subsemirings is their intersection.

                            Equations
                              @[simp]
                              theorem NonUnitalSubsemiring.coe_inf {R : Type u} [NonUnitalNonAssocSemiring R] (p p' : NonUnitalSubsemiring R) :
                              (pp') = p p'
                              @[simp]
                              theorem NonUnitalSubsemiring.mem_inf {R : Type u} [NonUnitalNonAssocSemiring R] {p p' : NonUnitalSubsemiring R} {x : R} :
                              x pp' x p x p'
                              def NonUnitalRingHom.codRestrict {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] [NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] {S' : Type u_2} [SetLike S' S] [NonUnitalSubsemiringClass S' S] (f : F) (s : S') (h : ∀ (x : R), f x s) :
                              R →ₙ+* s

                              Restriction of a non-unital ring homomorphism to a non-unital subsemiring of the codomain.

                              Equations
                                Instances For

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

                                  Equations
                                    Instances For

                                      The non-unital ring homomorphism associated to an inclusion of non-unital subsemirings.

                                      Equations
                                        Instances For