Documentation

Mathlib.Algebra.Ring.Submonoid.Pointwise

Elementwise monoid structure of additive submonoids #

These definitions are a cut-down versions of the ones around Submodule.mul, as that API is usually more useful.

SMul (AddSubmonoid R) (AddSubmonoid A) is also provided given DistribSMul R A, and when R = A it is definitionally equal to the multiplication on AddSubmonoid R.

These are all available in the Pointwise locale.

Additionally, it provides various degrees of monoid structure:

which is available globally to match the monoid structure implied by Submodule.idemSemiring.

Implementation notes #

Many results about multiplication are derived from the corresponding results about scalar multiplication, but results requiring right distributivity do not have SMul versions, due to the lack of a suitable typeclass (unless one goes all the way to Module).

If R is an additive monoid with one (e.g., a semiring), then 1 : AddSubmonoid R is the range of Nat.cast : ℕ → R.

Equations
    Instances For
      theorem AddSubmonoid.natCast_mem_one {R : Type u_2} [AddMonoidWithOne R] (n : ) :
      n 1
      @[simp]
      theorem AddSubmonoid.mem_one {R : Type u_2} [AddMonoidWithOne R] {x : R} :
      x 1 ∃ (n : ), n = x
      def AddSubmonoid.smul {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] :

      For M : Submonoid R and N : AddSubmonoid A, M • N is the additive submonoid generated by all m • n where m ∈ M and n ∈ N.

      Equations
        Instances For
          theorem AddSubmonoid.smul_mem_smul {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N : AddSubmonoid A} {m : R} {n : A} (hm : m M) (hn : n N) :
          m n M N
          theorem AddSubmonoid.smul_le {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N P : AddSubmonoid A} :
          M N P mM, nN, m n P
          theorem AddSubmonoid.smul_induction_on {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N : AddSubmonoid A} {C : AProp} {a : A} (ha : a M N) (hm : mM, nN, C (m n)) (hadd : ∀ (x y : A), C xC yC (x + y)) :
          C a
          @[simp]
          theorem AddSubmonoid.addSubmonoid_smul_bot {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] (S : AddSubmonoid R) :
          theorem AddSubmonoid.smul_le_smul {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M M' : AddSubmonoid R} {N P : AddSubmonoid A} (h : M M') (hnp : N P) :
          M N M' P
          theorem AddSubmonoid.smul_le_smul_left {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M M' : AddSubmonoid R} {P : AddSubmonoid A} (h : M M') :
          M P M' P
          theorem AddSubmonoid.smul_le_smul_right {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N P : AddSubmonoid A} (h : N P) :
          M N M P
          theorem AddSubmonoid.smul_subset_smul {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N : AddSubmonoid A} :
          M N ↑(M N)
          theorem AddSubmonoid.addSubmonoid_smul_sup {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N P : AddSubmonoid A} :
          M (NP) = M NM P
          theorem AddSubmonoid.smul_iSup {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {ι : Sort u_4} (T : AddSubmonoid R) (S : ιAddSubmonoid A) :
          T ⨆ (i : ι), S i = ⨆ (i : ι), T S i

          Multiplication of additive submonoids of a semiring R. The additive submonoid S * T is the smallest R-submodule of R containing the elements s * t for s ∈ S and t ∈ T.

          Equations
            Instances For
              theorem AddSubmonoid.mul_mem_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} {m n : R} (hm : m M) (hn : n N) :
              m * n M * N
              theorem AddSubmonoid.mul_le {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} :
              M * N P mM, nN, m * n P
              theorem AddSubmonoid.mul_induction_on {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} {C : RProp} {r : R} (hr : r M * N) (hm : mM, nN, C (m * n)) (ha : ∀ (x y : R), C xC yC (x + y)) :
              C r
              theorem AddSubmonoid.mul_le_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P Q : AddSubmonoid R} (hmp : M P) (hnq : N Q) :
              M * N P * Q
              theorem AddSubmonoid.mul_le_mul_left {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} (h : M N) :
              M * P N * P
              theorem AddSubmonoid.mul_le_mul_right {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} (h : N P) :
              M * N M * P
              theorem AddSubmonoid.mul_subset_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} :
              M * N ↑(M * N)
              theorem AddSubmonoid.mul_sup {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} :
              M * (NP) = M * NM * P
              theorem AddSubmonoid.sup_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} :
              (MN) * P = M * PN * P
              theorem AddSubmonoid.iSup_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] {ι : Sort u_4} (S : ιAddSubmonoid R) (T : AddSubmonoid R) :
              (⨆ (i : ι), S i) * T = ⨆ (i : ι), S i * T
              theorem AddSubmonoid.mul_iSup {R : Type u_2} [NonUnitalNonAssocSemiring R] {ι : Sort u_4} (T : AddSubmonoid R) (S : ιAddSubmonoid R) :
              T * ⨆ (i : ι), S i = ⨆ (i : ι), T * S i
              theorem AddSubmonoid.mul_comm_of_commute {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} (h : mM, nN, Commute m n) :
              M * N = N * M

              AddSubmonoid.neg distributes over multiplication.

              This is available as an instance in the Pointwise locale.

              Equations
                Instances For

                  A MulOneClass structure on additive submonoids of a (possibly, non-associative) semiring.

                  Equations
                    Instances For

                      Semigroup structure on additive submonoids of a (possibly, non-unital) semiring.

                      Equations
                        Instances For

                          Monoid structure on additive submonoids of a semiring.

                          Equations
                            Instances For
                              theorem AddSubmonoid.closure_pow {R : Type u_2} [Semiring R] (s : Set R) (n : ) :
                              closure s ^ n = closure (s ^ n)
                              theorem AddSubmonoid.pow_eq_closure_pow_set {R : Type u_2} [Semiring R] (s : AddSubmonoid R) (n : ) :
                              s ^ n = closure (s ^ n)
                              theorem AddSubmonoid.pow_subset_pow {R : Type u_2} [Semiring R] {s : AddSubmonoid R} {n : } :
                              s ^ n ↑(s ^ n)