Pointwise instances on Submonoids and AddSubmonoids

This file provides:

• Submonoid.inv
• AddSubmonoid.neg

and the actions

• Submonoid.pointwiseMulAction
• AddSubmonoid.pointwiseMulAction

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:

• AddSubmonoid.one
• AddSubmonoid.mul
• AddSubmonoid.mulOneClass
• AddSubmonoid.semigroup
• AddSubmonoid.monoid which is available globally to match the monoid structure implied by Submodule.idemSemiring.

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) : s * t ⊆ ↑(Submonoid.closure u)

theorem AddSubmonoid.add_subset_closure {M : Type u_3} [AddMonoid M] {s t u : Set M} (hs : s ⊆ u) (ht : t ⊆ u) : s + t ⊆ ↑(AddSubmonoid.closure 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_mul_le {M : Type u_3} [Monoid M] (S T : Set M) : Submonoid.closure (S * T) ≤ Submonoid.closure S ⊔ Submonoid.closure T

theorem AddSubmonoid.closure_add_le {M : Type u_3} [AddMonoid M] (S T : Set M) : AddSubmonoid.closure (S + T) ≤ AddSubmonoid.closure S ⊔ AddSubmonoid.closure T

theorem Submonoid.closure_pow_le {M : Type u_3} [Monoid M] {s : Set M} {n : ℕ} : n ≠ 0 → Submonoid.closure (s ^ n) ≤ Submonoid.closure s

theorem AddSubmonoid.closure_nsmul_le {M : Type u_3} [AddMonoid M] {s : Set M} {n : ℕ} : n ≠ 0 → AddSubmonoid.closure (n • s) ≤ AddSubmonoid.closure s

theorem Submonoid.closure_pow {M : Type u_3} [Monoid M] {s : Set M} {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : Submonoid.closure (s ^ n) = Submonoid.closure s

theorem AddSubmonoid.closure_nsmul {M : Type u_3} [AddMonoid M] {s : Set M} {n : ℕ} (hs : 0 ∈ s) (hn : n ≠ 0) : AddSubmonoid.closure (n • s) = AddSubmonoid.closure s

theorem Submonoid.sup_eq_closure_mul {M : Type u_3} [Monoid M] (H K : Submonoid M) : H ⊔ K = Submonoid.closure (↑H * ↑K)

theorem AddSubmonoid.sup_eq_closure_add {M : Type u_3} [AddMonoid M] (H K : AddSubmonoid M) : H ⊔ K = AddSubmonoid.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] : Inv (Submonoid G)

The submonoid with every element inverted.

Equations

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

def AddSubmonoid.neg {G : Type u_2} [AddGroup G] : Neg (AddSubmonoid G)

The additive submonoid with every element negated.

Equations

• AddSubmonoid.neg = { neg := fun (S : AddSubmonoid G) => { carrier := -↑S, add_mem' := ⋯, zero_mem' := ⋯ } }

@[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} : g ∈ S⁻¹ ↔ g⁻¹ ∈ S

@[simp]

theorem AddSubmonoid.mem_neg {G : Type u_2} [AddGroup G] {g : G} {S : AddSubmonoid G} : g ∈ -S ↔ -g ∈ S

def Submonoid.involutiveInv {G : Type u_2} [Group G] : InvolutiveInv (Submonoid G)

Inversion is involutive on submonoids.

Equations

• Submonoid.involutiveInv = Function.Injective.involutiveInv SetLike.coe ⋯ ⋯

def AddSubmonoid.involutiveNeg {G : Type u_2} [AddGroup G] : InvolutiveNeg (AddSubmonoid G)

Inversion is involutive on additive submonoids.

Equations

• AddSubmonoid.involutiveNeg = Function.Injective.involutiveNeg SetLike.coe ⋯ ⋯

@[simp]

theorem Submonoid.inv_le_inv {G : Type u_2} [Group G] (S T : Submonoid G) : S⁻¹ ≤ T⁻¹ ↔ S ≤ T

@[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) : S⁻¹ ≤ T ↔ S ≤ T⁻¹

theorem AddSubmonoid.neg_le {G : Type u_2} [AddGroup G] (S T : AddSubmonoid G) : -S ≤ T ↔ S ≤ -T

def Submonoid.invOrderIso {G : Type u_2} [Group G] : Submonoid G ≃o Submonoid G

Pointwise inversion of submonoids as an order isomorphism.

Equations

• Submonoid.invOrderIso = { toEquiv := Equiv.inv (Submonoid G), map_rel_iff' := ⋯ }

def AddSubmonoid.negOrderIso {G : Type u_2} [AddGroup G] : AddSubmonoid G ≃o AddSubmonoid G

Pointwise negation of additive submonoids as an order isomorphism

Equations

• AddSubmonoid.negOrderIso = { toEquiv := Equiv.neg (AddSubmonoid G), map_rel_iff' := ⋯ }

@[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✝

theorem Submonoid.closure_inv {G : Type u_2} [Group G] (s : Set G) : Submonoid.closure s⁻¹ = (Submonoid.closure s)⁻¹

theorem AddSubmonoid.closure_neg {G : Type u_2} [AddGroup G] (s : Set G) : AddSubmonoid.closure (-s) = -AddSubmonoid.closure s

@[simp]

theorem Submonoid.inv_inf {G : Type u_2} [Group G] (S T : Submonoid G) : (S ⊓ T)⁻¹ = S⁻¹ ⊓ T⁻¹

@[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) : (S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹

@[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

def Submonoid.pointwiseMulAction {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] : MulAction α (Submonoid M)

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

This is available as an instance in the Pointwise locale.

Equations

• Submonoid.pointwiseMulAction = MulAction.mk ⋯ ⋯

@[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 ∈ S → a • 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 ↔ ∃ s ∈ S, a • s = m

@[simp]

theorem Submonoid.smul_bot {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) : 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) : a • Submonoid.closure s = Submonoid.closure (a • s)

theorem Submonoid.pointwise_isCentralScalar {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] [MulDistribMulAction αᵐᵒᵖ M] [IsCentralScalar α M] : IsCentralScalar α (Submonoid 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

theorem Submonoid.mem_closure_inv {G : Type u_7} [Group G] (S : Set G) (x : G) : x ∈ Submonoid.closure S⁻¹ ↔ x⁻¹ ∈ Submonoid.closure S

theorem AddSubmonoid.mem_closure_neg {G : Type u_7} [AddGroup G] (S : Set G) (x : G) : x ∈ AddSubmonoid.closure (-S) ↔ -x ∈ AddSubmonoid.closure S

def AddSubmonoid.pointwiseMulAction {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] : MulAction α (AddSubmonoid A)

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

• AddSubmonoid.pointwiseMulAction = MulAction.mk ⋯ ⋯

@[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 ∈ S → a • 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 ↔ ∃ s ∈ S, a • s = m

@[simp]

theorem AddSubmonoid.smul_bot {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (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) : a • AddSubmonoid.closure s = AddSubmonoid.closure (a • s)

theorem AddSubmonoid.pointwise_isCentralScalar {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] [DistribMulAction αᵐᵒᵖ A] [IsCentralScalar α A] : IsCentralScalar α (AddSubmonoid 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.

def AddSubmonoid.one {R : Type u_4} [AddMonoidWithOne R] : One (AddSubmonoid R)

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

Equations

• AddSubmonoid.one = { one := AddMonoidHom.mrange (Nat.castAddMonoidHom R) }

theorem AddSubmonoid.one_eq_mrange {R : Type u_4} [AddMonoidWithOne R] : 1 = AddMonoidHom.mrange (Nat.castAddMonoidHom R)

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

theorem AddSubmonoid.one_eq_closure {R : Type u_4} [AddMonoidWithOne R] : 1 = AddSubmonoid.closure {1}

theorem AddSubmonoid.one_eq_closure_one_set {R : Type u_4} [AddMonoidWithOne R] : 1 = AddSubmonoid.closure 1

def AddSubmonoid.smul {R : Type u_4} {A : Type u_5} [AddMonoid A] [AddMonoid R] [DistribSMul R A] : SMul (AddSubmonoid R) (AddSubmonoid 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

• AddSubmonoid.smul = { smul := fun (M : AddSubmonoid R) (N : AddSubmonoid A) => ⨆ (s : ↥M), AddSubmonoid.map (DistribSMul.toAddMonoidHom A ↑s) N }

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 ↔ ∀ m ∈ M, ∀ n ∈ N, 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 : A → Prop} {a : A} (ha : a ∈ M • N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)) (hadd : ∀ (x y : A), C x → C y → C (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) : S • ⊥ = ⊥

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

def AddSubmonoid.mul {R : Type u_4} [NonUnitalNonAssocSemiring R] : Mul (AddSubmonoid R)

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

• AddSubmonoid.mul = { mul := fun (M N : AddSubmonoid R) => ⨆ (s : ↥M), AddSubmonoid.map (AddMonoidHom.mul ↑s) N }

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 ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P

theorem AddSubmonoid.mul_induction_on {R : Type u_4} [NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} {C : R → Prop} {r : R} (hr : r ∈ M * N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ (x y : R), C x → C y → C (x + y)) : C r

theorem AddSubmonoid.closure_mul_closure {R : Type u_4} [NonUnitalNonAssocSemiring R] (S T : Set R) : AddSubmonoid.closure S * AddSubmonoid.closure T = AddSubmonoid.closure (S * T)

theorem AddSubmonoid.mul_eq_closure_mul_set {R : Type u_4} [NonUnitalNonAssocSemiring R] (M N : AddSubmonoid R) : M * N = AddSubmonoid.closure (↑M * ↑N)

@[simp]

theorem AddSubmonoid.mul_bot {R : Type u_4} [NonUnitalNonAssocSemiring R] (S : AddSubmonoid R) : S * ⊥ = ⊥

@[simp]

theorem AddSubmonoid.bot_mul {R : Type u_4} [NonUnitalNonAssocSemiring R] (S : AddSubmonoid R) : ⊥ * S = ⊥

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 : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M

def AddSubmonoid.hasDistribNeg {R : Type u_4} [NonUnitalNonAssocRing R] : HasDistribNeg (AddSubmonoid R)

AddSubmonoid.neg distributes over multiplication.

This is available as an instance in the Pointwise locale.

Equations

• AddSubmonoid.hasDistribNeg = HasDistribNeg.mk ⋯ ⋯

def AddSubmonoid.mulOneClass {R : Type u_4} [NonAssocSemiring R] : MulOneClass (AddSubmonoid R)

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

Equations

• AddSubmonoid.mulOneClass = MulOneClass.mk ⋯ ⋯

def AddSubmonoid.semigroup {R : Type u_4} [NonUnitalSemiring R] : Semigroup (AddSubmonoid R)

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

Equations

• AddSubmonoid.semigroup = Semigroup.mk ⋯

def AddSubmonoid.monoid {R : Type u_4} [Semiring R] : Monoid (AddSubmonoid R)

Monoid structure on additive submonoids of a semiring.

Equations

• AddSubmonoid.monoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

theorem AddSubmonoid.closure_pow {R : Type u_4} [Semiring R] (s : Set R) (n : ℕ) : AddSubmonoid.closure s ^ n = AddSubmonoid.closure (s ^ n)

theorem AddSubmonoid.pow_eq_closure_pow_set {R : Type u_4} [Semiring R] (s : AddSubmonoid R) (n : ℕ) : s ^ n = AddSubmonoid.closure (↑s ^ n)

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 : ∀ x ∈ s, 1 ≤ x) (h : s.IsPWO) : (↑(Submonoid.closure s)).IsPWO

theorem Set.IsPWO.addSubmonoid_closure {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} (hpos : ∀ x ∈ s, 0 ≤ x) (h : s.IsPWO) : (↑(AddSubmonoid.closure s)).IsPWO