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.

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.

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 AddSubmonoid.add_subset {M : Type u_3} [AddMonoid M] {s : Set M} {t : Set M} {S : AddSubmonoid M} (hs : s ⊆ ↑S) (ht : t ⊆ ↑S) : s + t ⊆ ↑S

theorem Submonoid.mul_subset {M : Type u_3} [Monoid M] {s : Set M} {t : Set M} {S : Submonoid M} (hs : s ⊆ ↑S) (ht : t ⊆ ↑S) : s * t ⊆ ↑S

theorem AddSubmonoid.add_subset_closure {M : Type u_3} [AddMonoid M] {s : Set M} {t : Set M} {u : Set M} (hs : s ⊆ u) (ht : t ⊆ u) : s + t ⊆ ↑(AddSubmonoid.closure u)

theorem Submonoid.mul_subset_closure {M : Type u_3} [Monoid M] {s : Set M} {t : Set M} {u : Set M} (hs : s ⊆ u) (ht : t ⊆ u) : s * t ⊆ ↑(Submonoid.closure u)

theorem AddSubmonoid.coe_add_self_eq {M : Type u_3} [AddMonoid M] (s : AddSubmonoid M) : ↑s + ↑s = ↑s

theorem Submonoid.coe_mul_self_eq {M : Type u_3} [Monoid M] (s : Submonoid M) : ↑s * ↑s = ↑s

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

abbrev AddSubmonoid.closure_add_le.match_1 {M : Type u_1} [AddMonoid M] (S : Set M) (T : Set M) (_x : M) (motive : _x ∈ S + T → Prop) : ∀ (x : _x ∈ S + T), (∀ (_s : M) (hs : _s ∈ S) (_t : M) (ht : _t ∈ T) (hx : (fun (x x_1 : M) => x + x_1) _s _t = _x), motive (_ : ∃ a ∈ S, ∃ b ∈ T, (fun (x x_1 : M) => x + x_1) a b = _x)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem Submonoid.closure_mul_le {M : Type u_3} [Monoid M] (S : Set M) (T : Set M) : Submonoid.closure (S * T) ≤ Submonoid.closure S ⊔ Submonoid.closure T

theorem AddSubmonoid.sup_eq_closure_add {M : Type u_3} [AddMonoid M] (H : AddSubmonoid M) (K : AddSubmonoid M) : H ⊔ K = AddSubmonoid.closure (↑H + ↑K)

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

theorem AddSubmonoid.nsmul_vadd_mem_closure_vadd {M : Type u_3} [AddMonoid M] {N : Type u_6} [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)

theorem Submonoid.pow_smul_mem_closure_smul {M : Type u_3} [Monoid M] {N : Type u_6} [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.neg.proof_1 {G : Type u_1} [AddGroup G] (S : AddSubmonoid G) : ∀ {a b : G}, a ∈ -↑S → b ∈ -↑S → a + b ∈ -↑S

theorem AddSubmonoid.neg.proof_2 {G : Type u_1} [AddGroup G] (S : AddSubmonoid G) : 0 ∈ -↑S

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

The additive submonoid with every element negated.

Equations

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

def Submonoid.inv {G : Type u_2} [Group G] : Inv (Submonoid G)

The submonoid with every element inverted.

Equations

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

@[simp]

theorem AddSubmonoid.coe_neg {G : Type u_2} [AddGroup G] (S : AddSubmonoid G) : ↑(-S) = -↑S

@[simp]

theorem Submonoid.coe_inv {G : Type u_2} [Group G] (S : Submonoid G) : ↑S⁻¹ = (↑S)⁻¹

@[simp]

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

@[simp]

theorem Submonoid.mem_inv {G : Type u_2} [Group G] {g : G} {S : Submonoid G} : g ∈ S⁻¹ ↔ g⁻¹ ∈ S

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 (_ : Function.Injective SetLike.coe) (_ : ∀ (x : AddSubmonoid G), ↑(-x) = ↑(-x))

theorem AddSubmonoid.involutiveNeg.proof_1 {G : Type u_1} [AddGroup G] : Function.Injective SetLike.coe

theorem AddSubmonoid.involutiveNeg.proof_2 {G : Type u_1} [AddGroup G] : ∀ (x : AddSubmonoid G), ↑(-x) = ↑(-x)

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 (_ : Function.Injective SetLike.coe) (_ : ∀ (x : Submonoid G), ↑x⁻¹ = ↑x⁻¹)

@[simp]

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

@[simp]

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

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

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

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' := (_ : ∀ {a b : AddSubmonoid G}, -a ≤ -b ↔ a ≤ b) }

@[simp]

theorem AddSubmonoid.negOrderIso_apply_coe {G : Type u_2} [AddGroup G] : ∀ (a : AddSubmonoid G), ↑(AddSubmonoid.negOrderIso a) = -↑a

@[simp]

theorem AddSubmonoid.negOrderIso_symm_apply_coe {G : Type u_2} [AddGroup G] : ∀ (a : AddSubmonoid G), ↑((RelIso.symm AddSubmonoid.negOrderIso) a) = -↑a

@[simp]

theorem Submonoid.invOrderIso_apply_coe {G : Type u_2} [Group G] : ∀ (a : Submonoid G), ↑(Submonoid.invOrderIso a) = (↑a)⁻¹

@[simp]

theorem Submonoid.invOrderIso_symm_apply_coe {G : Type u_2} [Group G] : ∀ (a : Submonoid G), ↑((RelIso.symm Submonoid.invOrderIso) a) = (↑a)⁻¹

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' := (_ : ∀ {a b : Submonoid G}, a⁻¹ ≤ b⁻¹ ↔ a ≤ b) }

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

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

@[simp]

theorem AddSubmonoid.neg_inf {G : Type u_2} [AddGroup G] (S : AddSubmonoid G) (T : AddSubmonoid G) : -(S ⊓ T) = -S ⊓ -T

@[simp]

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

@[simp]

theorem AddSubmonoid.neg_sup {G : Type u_2} [AddGroup G] (S : AddSubmonoid G) (T : AddSubmonoid G) : -(S ⊔ T) = -S ⊔ -T

@[simp]

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

@[simp]

theorem AddSubmonoid.neg_bot {G : Type u_2} [AddGroup G] : -⊥ = ⊥

@[simp]

theorem Submonoid.inv_bot {G : Type u_2} [Group G] : ⊥⁻¹ = ⊥

@[simp]

theorem AddSubmonoid.neg_top {G : Type u_2} [AddGroup G] : -⊤ = ⊤

@[simp]

theorem Submonoid.inv_top {G : Type u_2} [Group G] : ⊤⁻¹ = ⊤

@[simp]

theorem AddSubmonoid.neg_iInf {G : Type u_2} [AddGroup G] {ι : Sort u_6} (S : ι → AddSubmonoid G) : -⨅ (i : ι), S i = ⨅ (i : ι), -S i

@[simp]

theorem Submonoid.inv_iInf {G : Type u_2} [Group G] {ι : Sort u_6} (S : ι → Submonoid G) : (⨅ (i : ι), S i)⁻¹ = ⨅ (i : ι), (S i)⁻¹

@[simp]

theorem AddSubmonoid.neg_iSup {G : Type u_2} [AddGroup G] {ι : Sort u_6} (S : ι → AddSubmonoid G) : -⨆ (i : ι), S i = ⨆ (i : ι), -S i

@[simp]

theorem Submonoid.inv_iSup {G : Type u_2} [Group G] {ι : Sort u_6} (S : ι → Submonoid 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

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

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

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 : Submonoid M) (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 : Submonoid M} {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 : Submonoid M} {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 : Submonoid M} {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 : Submonoid M} {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 : Submonoid M} {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 : Submonoid M} {T : Submonoid M} : S ≤ a • T ↔ a⁻¹ • S ≤ T

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

theorem Submonoid.mem_closure_inv {G : Type u_6} [Group G] (S : Set G) (x : G) : x ∈ Submonoid.closure S⁻¹ ↔ x⁻¹ ∈ Submonoid.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

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

@[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 : AddSubmonoid A) (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 : AddSubmonoid A} {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 : AddSubmonoid A} {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 : AddSubmonoid A} {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 : AddSubmonoid A} {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 : AddSubmonoid A} {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 : AddSubmonoid A} {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.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 : AddSubmonoid R} {N : AddSubmonoid R} {m : R} {n : R} (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N

theorem AddSubmonoid.mul_le {R : Type u_4} [NonUnitalNonAssocSemiring R] {M : AddSubmonoid R} {N : AddSubmonoid R} {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 : AddSubmonoid R} {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 : Set R) (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 : AddSubmonoid R) (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 : AddSubmonoid R} {N : AddSubmonoid R} {P : AddSubmonoid R} {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 : AddSubmonoid R} {N : AddSubmonoid R} {P : AddSubmonoid R} (h : M ≤ N) : M * P ≤ N * P

theorem AddSubmonoid.mul_le_mul_right {R : Type u_4} [NonUnitalNonAssocSemiring R] {M : AddSubmonoid R} {N : AddSubmonoid R} {P : AddSubmonoid R} (h : N ≤ P) : M * N ≤ M * P

theorem AddSubmonoid.mul_subset_mul {R : Type u_4} [NonUnitalNonAssocSemiring R] {M : AddSubmonoid R} {N : AddSubmonoid R} : ↑M * ↑N ⊆ ↑(M * N)

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 = let src := AddSubmonoid.involutiveNeg; HasDistribNeg.mk (_ : ∀ (x y : AddSubmonoid R), -x * y = -(x * y)) (_ : ∀ (x y : AddSubmonoid R), x * -y = -(x * y))

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 (_ : ∀ (M : AddSubmonoid R), 1 * M = M) (_ : ∀ (M : AddSubmonoid R), M * 1 = M)

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 (_ : ∀ (M N P : AddSubmonoid R), M * N * P = M * (N * P))

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

Monoid structure on additive submonoids of a semiring.

Equations

• AddSubmonoid.monoid = let src := AddSubmonoid.semigroup; let src_1 := AddSubmonoid.mulOneClass; Monoid.mk (_ : ∀ (a : AddSubmonoid R), 1 * a = a) (_ : ∀ (a : AddSubmonoid R), a * 1 = a) npowRec

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.addSubmonoid_closure {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} (hpos : ∀ x ∈ s, 0 ≤ x) (h : Set.IsPWO s) : Set.IsPWO ↑(AddSubmonoid.closure s)

theorem Set.IsPWO.submonoid_closure {α : Type u_1} [OrderedCancelCommMonoid α] {s : Set α} (hpos : ∀ x ∈ s, 1 ≤ x) (h : Set.IsPWO s) : Set.IsPWO ↑(Submonoid.closure s)