Documentation

Mathlib.Algebra.Group.Submonoid.Pointwise

Pointwise instances on Submonoids and AddSubmonoids #

This file provides:

and the actions

which matches the action of Set.mulActionSet.

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:

Implementation notes #

Most of the lemmas in this file are direct copies of lemmas from Algebra/Pointwise.lean. While the statements of these lemmas are defeq, we repeat them here due to them not being syntactically equal. Before adding new lemmas here, consider if they would also apply to the action on Sets.

Many results about multiplication is 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).

@[simp]
theorem coe_mul_coe {M : Type u_3} {S : Type u_6} [Monoid M] [SetLike S M] [SubmonoidClass S M] (H : S) :
H * H = H
@[simp]
theorem coe_add_coe {M : Type u_3} {S : Type u_6} [AddMonoid M] [SetLike S M] [AddSubmonoidClass S M] (H : S) :
H + H = H
@[simp]
theorem coe_set_pow {M : Type u_3} {S : Type u_6} [Monoid M] [SetLike S M] [SubmonoidClass S M] {n : } (hn : n 0) (H : S) :
H ^ n = H
@[simp]
theorem coe_set_nsmul {M : Type u_3} {S : Type u_6} [AddMonoid M] [SetLike S M] [AddSubmonoidClass S M] {n : } (hn : n 0) (H : S) :
n H = H

Some lemmas about pointwise multiplication and submonoids. Ideally we put these in GroupTheory.Submonoid.Basic, but currently we cannot because that file is imported by this.

theorem Submonoid.mul_subset {M : Type u_3} [Monoid M] {s t : Set M} {S : Submonoid M} (hs : s S) (ht : t S) :
s * t S
theorem AddSubmonoid.add_subset {M : Type u_3} [AddMonoid M] {s t : Set M} {S : AddSubmonoid M} (hs : s S) (ht : t S) :
s + t S
theorem Submonoid.mul_subset_closure {M : Type u_3} [Monoid M] {s t u : Set M} (hs : s u) (ht : t u) :
theorem AddSubmonoid.add_subset_closure {M : Type u_3} [AddMonoid M] {s t u : Set M} (hs : s u) (ht : t u) :
theorem Submonoid.coe_mul_self_eq {M : Type u_3} [Monoid M] (s : Submonoid M) :
s * s = s
theorem AddSubmonoid.coe_add_self_eq {M : Type u_3} [AddMonoid M] (s : AddSubmonoid M) :
s + s = s
theorem Submonoid.closure_pow_le {M : Type u_3} [Monoid M] {s : Set M} {n : } :
theorem Submonoid.closure_pow {M : Type u_3} [Monoid M] {s : Set M} {n : } (hs : 1 s) (hn : n 0) :
theorem AddSubmonoid.closure_nsmul {M : Type u_3} [AddMonoid M] {s : Set M} {n : } (hs : 0 s) (hn : n 0) :
theorem Submonoid.sup_eq_closure_mul {M : Type u_3} [Monoid M] (H K : Submonoid M) :
H K = Submonoid.closure (H * K)
theorem Submonoid.pow_smul_mem_closure_smul {M : Type u_3} [Monoid M] {N : Type u_7} [CommMonoid N] [MulAction M N] [IsScalarTower M N N] (r : M) (s : Set N) {x : N} (hx : x Submonoid.closure s) :
∃ (n : ), r ^ n x Submonoid.closure (r s)
theorem AddSubmonoid.nsmul_vadd_mem_closure_vadd {M : Type u_3} [AddMonoid M] {N : Type u_7} [AddCommMonoid N] [AddAction M N] [VAddAssocClass M N N] (r : M) (s : Set N) {x : N} (hx : x AddSubmonoid.closure s) :
∃ (n : ), n r +ᵥ x AddSubmonoid.closure (r +ᵥ s)
def Submonoid.inv {G : Type u_2} [Group G] :

The submonoid with every element inverted.

Equations
  • Submonoid.inv = { inv := fun (S : Submonoid G) => { carrier := (↑S)⁻¹, mul_mem' := , one_mem' := } }
Instances For

    The additive submonoid with every element negated.

    Equations
    • AddSubmonoid.neg = { neg := fun (S : AddSubmonoid G) => { carrier := -S, add_mem' := , zero_mem' := } }
    Instances For
      @[simp]
      theorem Submonoid.coe_inv {G : Type u_2} [Group G] (S : Submonoid G) :
      S⁻¹ = (↑S)⁻¹
      @[simp]
      theorem AddSubmonoid.coe_neg {G : Type u_2} [AddGroup G] (S : AddSubmonoid G) :
      (-S) = -S
      @[simp]
      theorem Submonoid.mem_inv {G : Type u_2} [Group G] {g : G} {S : Submonoid G} :
      @[simp]
      theorem AddSubmonoid.mem_neg {G : Type u_2} [AddGroup G] {g : G} {S : AddSubmonoid G} :
      g -S -g S

      Inversion is involutive on submonoids.

      Equations
      Instances For

        Inversion is involutive on additive submonoids.

        Equations
        Instances For
          @[simp]
          theorem Submonoid.inv_le_inv {G : Type u_2} [Group G] (S T : Submonoid G) :
          @[simp]
          theorem AddSubmonoid.neg_le_neg {G : Type u_2} [AddGroup G] (S T : AddSubmonoid G) :
          -S -T S T
          theorem Submonoid.inv_le {G : Type u_2} [Group G] (S T : Submonoid G) :
          theorem AddSubmonoid.neg_le {G : Type u_2} [AddGroup G] (S T : AddSubmonoid G) :
          -S T S -T

          Pointwise inversion of submonoids as an order isomorphism.

          Equations
          Instances For

            Pointwise negation of additive submonoids as an order isomorphism

            Equations
            Instances For
              @[simp]
              theorem Submonoid.coe_invOrderIso_apply {G : Type u_2} [Group G] (a✝ : Submonoid G) :
              (Submonoid.invOrderIso a✝) = (↑a✝)⁻¹
              @[simp]
              theorem Submonoid.coe_invOrderIso_symm_apply {G : Type u_2} [Group G] (a✝ : Submonoid G) :
              ((RelIso.symm Submonoid.invOrderIso) a✝) = (↑a✝)⁻¹
              @[simp]
              theorem AddSubmonoid.coe_negOrderIso_apply {G : Type u_2} [AddGroup G] (a✝ : AddSubmonoid G) :
              (AddSubmonoid.negOrderIso a✝) = -a✝
              @[simp]
              theorem AddSubmonoid.coe_negOrderIso_symm_apply {G : Type u_2} [AddGroup G] (a✝ : AddSubmonoid G) :
              ((RelIso.symm AddSubmonoid.negOrderIso) a✝) = -a✝
              @[simp]
              theorem Submonoid.inv_inf {G : Type u_2} [Group G] (S T : Submonoid G) :
              @[simp]
              theorem AddSubmonoid.neg_inf {G : Type u_2} [AddGroup G] (S T : AddSubmonoid G) :
              -(S T) = -S -T
              @[simp]
              theorem Submonoid.inv_sup {G : Type u_2} [Group G] (S T : Submonoid G) :
              @[simp]
              theorem AddSubmonoid.neg_sup {G : Type u_2} [AddGroup G] (S T : AddSubmonoid G) :
              -(S T) = -S -T
              @[simp]
              theorem Submonoid.inv_bot {G : Type u_2} [Group G] :
              @[simp]
              theorem AddSubmonoid.neg_bot {G : Type u_2} [AddGroup G] :
              @[simp]
              theorem Submonoid.inv_top {G : Type u_2} [Group G] :
              @[simp]
              theorem AddSubmonoid.neg_top {G : Type u_2} [AddGroup G] :
              @[simp]
              theorem Submonoid.inv_iInf {G : Type u_2} [Group G] {ι : Sort u_7} (S : ιSubmonoid G) :
              (⨅ (i : ι), S i)⁻¹ = ⨅ (i : ι), (S i)⁻¹
              @[simp]
              theorem AddSubmonoid.neg_iInf {G : Type u_2} [AddGroup G] {ι : Sort u_7} (S : ιAddSubmonoid G) :
              -⨅ (i : ι), S i = ⨅ (i : ι), -S i
              @[simp]
              theorem Submonoid.inv_iSup {G : Type u_2} [Group G] {ι : Sort u_7} (S : ιSubmonoid G) :
              (⨆ (i : ι), S i)⁻¹ = ⨆ (i : ι), (S i)⁻¹
              @[simp]
              theorem AddSubmonoid.neg_iSup {G : Type u_2} [AddGroup G] {ι : Sort u_7} (S : ιAddSubmonoid G) :
              -⨆ (i : ι), S i = ⨆ (i : ι), -S i

              The action on a submonoid corresponding to applying the action to every element.

              This is available as an instance in the Pointwise locale.

              Equations
              Instances For
                @[simp]
                theorem Submonoid.coe_pointwise_smul {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) (S : Submonoid M) :
                (a S) = a S
                theorem Submonoid.smul_mem_pointwise_smul {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (m : M) (a : α) (S : Submonoid M) :
                m Sa m a S
                instance Submonoid.instCovariantClassHSMulLe {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] :
                CovariantClass α (Submonoid M) HSMul.hSMul LE.le
                theorem Submonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (m : M) (a : α) (S : Submonoid M) :
                m a S sS, a s = m
                @[simp]
                theorem Submonoid.smul_bot {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) :
                theorem Submonoid.smul_sup {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) (S T : Submonoid M) :
                a (S T) = a S a T
                theorem Submonoid.smul_closure {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) (s : Set M) :
                @[simp]
                theorem Submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {x : M} :
                a x a S x S
                theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {x : M} :
                x a S a⁻¹ x S
                theorem Submonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {x : M} :
                x a⁻¹ S a x S
                @[simp]
                theorem Submonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S T : Submonoid M} :
                a S a T S T
                theorem Submonoid.pointwise_smul_subset_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S T : Submonoid M} :
                a S T S a⁻¹ T
                theorem Submonoid.subset_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S T : Submonoid M} :
                S a T a⁻¹ S T
                @[simp]
                theorem Submonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) (S : Submonoid M) (x : M) :
                a x a S x S
                theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) (S : Submonoid M) (x : M) :
                x a S a⁻¹ x S
                theorem Submonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) (S : Submonoid M) (x : M) :
                x a⁻¹ S a x S
                @[simp]
                theorem Submonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) {S T : Submonoid M} :
                a S a T S T
                theorem Submonoid.pointwise_smul_le_iff₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) {S T : Submonoid M} :
                a S T S a⁻¹ T
                theorem Submonoid.le_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) {S T : Submonoid M} :
                S a T a⁻¹ S T

                The action on an additive submonoid corresponding to applying the action to every element.

                This is available as an instance in the Pointwise locale.

                Equations
                Instances For
                  @[simp]
                  theorem AddSubmonoid.coe_pointwise_smul {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (a : α) (S : AddSubmonoid A) :
                  (a S) = a S
                  theorem AddSubmonoid.smul_mem_pointwise_smul {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (m : A) (a : α) (S : AddSubmonoid A) :
                  m Sa m a S
                  theorem AddSubmonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (m : A) (a : α) (S : AddSubmonoid A) :
                  m a S sS, a s = m
                  @[simp]
                  theorem AddSubmonoid.smul_bot {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (a : α) :
                  theorem AddSubmonoid.smul_sup {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (a : α) (S T : AddSubmonoid A) :
                  a (S T) = a S a T
                  @[simp]
                  theorem AddSubmonoid.smul_closure {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (a : α) (s : Set A) :
                  @[simp]
                  theorem AddSubmonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubmonoid A} {x : A} :
                  a x a S x S
                  theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubmonoid A} {x : A} :
                  x a S a⁻¹ x S
                  theorem AddSubmonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubmonoid A} {x : A} :
                  x a⁻¹ S a x S
                  @[simp]
                  theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S T : AddSubmonoid A} :
                  a S a T S T
                  theorem AddSubmonoid.pointwise_smul_le_iff {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S T : AddSubmonoid A} :
                  a S T S a⁻¹ T
                  theorem AddSubmonoid.le_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S T : AddSubmonoid A} :
                  S a T a⁻¹ S T
                  @[simp]
                  theorem AddSubmonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) (S : AddSubmonoid A) (x : A) :
                  a x a S x S
                  theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) (S : AddSubmonoid A) (x : A) :
                  x a S a⁻¹ x S
                  theorem AddSubmonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) (S : AddSubmonoid A) (x : A) :
                  x a⁻¹ S a x S
                  @[simp]
                  theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) {S T : AddSubmonoid A} :
                  a S a T S T
                  theorem AddSubmonoid.pointwise_smul_le_iff₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) {S T : AddSubmonoid A} :
                  a S T S a⁻¹ T
                  theorem AddSubmonoid.le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) {S T : AddSubmonoid A} :
                  S a T a⁻¹ S T

                  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.

                  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_4} [AddMonoidWithOne R] (n : ) :
                    n 1
                    @[simp]
                    theorem AddSubmonoid.mem_one {R : Type u_4} [AddMonoidWithOne R] {x : R} :
                    x 1 ∃ (n : ), n = x
                    def AddSubmonoid.smul {R : Type u_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [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_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [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_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [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_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [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_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [DistribSMul R A] (S : AddSubmonoid R) :
                      theorem AddSubmonoid.smul_le_smul {R : Type u_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [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_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [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_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [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_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [DistribSMul R A] {M : AddSubmonoid R} {N : AddSubmonoid A} :
                      M N (M N)
                      theorem AddSubmonoid.addSubmonoid_smul_sup {R : Type u_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [DistribSMul R A] {M : AddSubmonoid R} {N P : AddSubmonoid A} :
                      M (N P) = M N M P
                      theorem AddSubmonoid.smul_iSup {R : Type u_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [DistribSMul R A] {ι : Sort u_7} (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_4} [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_4} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} :
                        M * N P mM, nN, m * n P
                        theorem AddSubmonoid.mul_induction_on {R : Type u_4} [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_4} [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_4} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} (h : M N) :
                        M * P N * P
                        theorem AddSubmonoid.mul_le_mul_right {R : Type u_4} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} (h : N P) :
                        M * N M * P
                        theorem AddSubmonoid.mul_subset_mul {R : Type u_4} [NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} :
                        M * N (M * N)
                        theorem AddSubmonoid.mul_sup {R : Type u_4} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} :
                        M * (N P) = M * N M * P
                        theorem AddSubmonoid.sup_mul {R : Type u_4} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} :
                        (M N) * P = M * P N * P
                        theorem AddSubmonoid.iSup_mul {R : Type u_4} [NonUnitalNonAssocSemiring R] {ι : Sort u_7} (S : ιAddSubmonoid R) (T : AddSubmonoid R) :
                        (⨆ (i : ι), S i) * T = ⨆ (i : ι), S i * T
                        theorem AddSubmonoid.mul_iSup {R : Type u_4} [NonUnitalNonAssocSemiring R] {ι : Sort u_7} (T : AddSubmonoid R) (S : ιAddSubmonoid R) :
                        T * ⨆ (i : ι), S i = ⨆ (i : ι), T * S i
                        theorem AddSubmonoid.mul_comm_of_commute {R : Type u_4} [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
                              • AddSubmonoid.monoid = Monoid.mk npowRecAuto
                              Instances For
                                theorem AddSubmonoid.pow_subset_pow {R : Type u_4} [Semiring R] {s : AddSubmonoid R} {n : } :
                                s ^ n (s ^ n)
                                theorem Set.IsPWO.submonoid_closure {α : Type u_1} [OrderedCancelCommMonoid α] {s : Set α} (hpos : xs, 1 x) (h : s.IsPWO) :
                                (↑(Submonoid.closure s)).IsPWO
                                theorem Set.IsPWO.addSubmonoid_closure {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} (hpos : xs, 0 x) (h : s.IsPWO) :
                                (↑(AddSubmonoid.closure s)).IsPWO