mathlib3 documentation

group_theory.submonoid.pointwise

Pointwise instances on `submonoid`s and `add_submonoid`s #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides:

and the actions

which matches the action of mul_action_set.

These are all available in the pointwise locale.

Additionally, it provides various degrees of monoid structure:

add_submonoid.has_one
add_submonoid.has_mul
add_submonoid.mul_one_class
add_submonoid.semigroup
add_submonoid.monoid which is available globally to match the monoid structure implied by submodule.idem_semiring.

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 group_theory.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 add_submonoid.add_subset {M : Type u_3} [add_monoid M] {s t : set M} {S : add_submonoid M} (hs : s ⊆ ↑S) (ht : t ⊆ ↑S) :

s + t ⊆ ↑S

theorem add_submonoid.add_subset_closure {M : Type u_3} [add_monoid M] {s t u : set M} (hs : s ⊆ u) (ht : t ⊆ u) :

s + t ⊆ ↑(add_submonoid.closure u)

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 add_submonoid.coe_add_self_eq {M : Type u_3} [add_monoid M] (s : add_submonoid M) :

↑s + ↑s = ↑s

theorem submonoid.coe_mul_self_eq {M : Type u_3} [monoid M] (s : submonoid M) :

↑s * ↑s = ↑s

theorem add_submonoid.closure_add_le {M : Type u_3} [add_monoid M] (S T : set M) :

add_submonoid.closure (S + T) ≤ add_submonoid.closure S ⊔ add_submonoid.closure T

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 add_submonoid.sup_eq_closure {M : Type u_3} [add_monoid M] (H K : add_submonoid M) :

H ⊔ K = add_submonoid.closure (↑H + ↑K)

theorem submonoid.sup_eq_closure {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_1} [comm_monoid N] [mul_action M N] [is_scalar_tower M N N] (r : M) (s : set N) {x : N} (hx : x ∈ submonoid.closure s) :

∃ (n : ℕ), r ^ n • x ∈ submonoid.closure (r • s)

theorem add_submonoid.nsmul_vadd_mem_closure_vadd {M : Type u_3} [add_monoid M] {N : Type u_1} [add_comm_monoid N] [add_action M N] [vadd_assoc_class M N N] (r : M) (s : set N) {x : N} (hx : x ∈ add_submonoid.closure s) :

∃ (n : ℕ), n • r +ᵥ x ∈ add_submonoid.closure (r +ᵥ s)

@[protected]

def add_submonoid.has_neg {G : Type u_2} [add_group G] :

has_neg (add_submonoid G)

The additive submonoid with every element negated.

Equations

add_submonoid.has_neg = {neg := λ (S : add_submonoid G), {carrier := -↑S, add_mem' := _, zero_mem' := _}}

@[protected]

def submonoid.has_inv {G : Type u_2} [group G] :

has_inv (submonoid G)

The submonoid with every element inverted.

Equations

submonoid.has_inv = {inv := λ (S : submonoid G), {carrier := (↑S)⁻¹, mul_mem' := _, one_mem' := _}}

@[simp]

theorem add_submonoid.coe_neg {G : Type u_2} [add_group G] (S : add_submonoid G) :

@[simp]

theorem submonoid.coe_inv {G : Type u_2} [group G] (S : submonoid 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 add_submonoid.mem_neg {G : Type u_2} [add_group G] {g : G} {S : add_submonoid G} :

g ∈ -S ↔ -g ∈ S

@[protected, instance]

def submonoid.has_involutive_inv {G : Type u_2} [group G] :

has_involutive_inv (submonoid G)

Equations

submonoid.has_involutive_inv = function.injective.has_involutive_inv coe submonoid.has_involutive_inv._proof_1 submonoid.has_involutive_inv._proof_2

@[protected, instance]

def add_submonoid.has_involutive_neg {G : Type u_2} [add_group G] :

has_involutive_neg (add_submonoid G)

Equations

add_submonoid.has_involutive_neg = function.injective.has_involutive_neg coe add_submonoid.has_involutive_neg._proof_1 add_submonoid.has_involutive_neg._proof_2

@[simp]

theorem submonoid.inv_le_inv {G : Type u_2} [group G] (S T : submonoid G) :

S⁻¹ ≤ T⁻¹ ↔ S ≤ T

@[simp]

theorem add_submonoid.neg_le_neg {G : Type u_2} [add_group G] (S T : add_submonoid G) :

-S ≤ -T ↔ S ≤ T

theorem submonoid.inv_le {G : Type u_2} [group G] (S T : submonoid G) :

S⁻¹ ≤ T ↔ S ≤ T⁻¹

theorem add_submonoid.neg_le {G : Type u_2} [add_group G] (S T : add_submonoid G) :

-S ≤ T ↔ S ≤ -T

def add_submonoid.neg_order_iso {G : Type u_2} [add_group G] :

add_submonoid G ≃o add_submonoid G

add_submonoid.has_neg as an order isomorphism

Equations

add_submonoid.neg_order_iso = {to_equiv := equiv.neg (add_submonoid G) add_submonoid.has_involutive_neg, map_rel_iff' := _}

@[simp]

theorem add_submonoid.neg_order_iso_apply_coe {G : Type u_2} [add_group G] (ᾰ : add_submonoid G) :

↑(⇑add_submonoid.neg_order_iso ᾰ) = -↑ᾰ

@[simp]

theorem add_submonoid.neg_order_iso_symm_apply_coe {G : Type u_2} [add_group G] (ᾰ : add_submonoid G) :

↑(⇑(rel_iso.symm add_submonoid.neg_order_iso) ᾰ) = -↑ᾰ

@[simp]

theorem submonoid.inv_order_iso_symm_apply_coe {G : Type u_2} [group G] (ᾰ : submonoid G) :

↑(⇑(rel_iso.symm submonoid.inv_order_iso) ᾰ) = (↑ᾰ)⁻¹

@[simp]

theorem submonoid.inv_order_iso_apply_coe {G : Type u_2} [group G] (ᾰ : submonoid G) :

↑(⇑submonoid.inv_order_iso ᾰ) = (↑ᾰ)⁻¹

def submonoid.inv_order_iso {G : Type u_2} [group G] :

submonoid G ≃o submonoid G

submonoid.has_inv as an order isomorphism.

Equations

submonoid.inv_order_iso = {to_equiv := equiv.inv (submonoid G) submonoid.has_involutive_inv, map_rel_iff' := _}

theorem add_submonoid.closure_neg {G : Type u_2} [add_group G] (s : set G) :

add_submonoid.closure (-s) = -add_submonoid.closure s

theorem submonoid.closure_inv {G : Type u_2} [group G] (s : set G) :

submonoid.closure s⁻¹ = (submonoid.closure s)⁻¹

@[simp]

theorem add_submonoid.neg_inf {G : Type u_2} [add_group G] (S T : add_submonoid G) :

-(S ⊓ T) = -S ⊓ -T

@[simp]

theorem submonoid.inv_inf {G : Type u_2} [group G] (S T : submonoid 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 add_submonoid.neg_sup {G : Type u_2} [add_group G] (S T : add_submonoid G) :

-(S ⊔ T) = -S ⊔ -T

@[simp]

theorem submonoid.inv_bot {G : Type u_2} [group G] :

@[simp]

theorem add_submonoid.neg_bot {G : Type u_2} [add_group G] :

@[simp]

theorem add_submonoid.neg_top {G : Type u_2} [add_group G] :

@[simp]

theorem submonoid.inv_top {G : Type u_2} [group G] :

@[simp]

theorem submonoid.inv_infi {G : Type u_2} [group G] {ι : Sort u_1} (S : ι → submonoid G) :

(⨅ (i : ι), S i)⁻¹ = ⨅ (i : ι), (S i)⁻¹

@[simp]

theorem add_submonoid.neg_infi {G : Type u_2} [add_group G] {ι : Sort u_1} (S : ι → add_submonoid G) :

(-⨅ (i : ι), S i) = ⨅ (i : ι), -S i

@[simp]

theorem submonoid.inv_supr {G : Type u_2} [group G] {ι : Sort u_1} (S : ι → submonoid G) :

(⨆ (i : ι), S i)⁻¹ = ⨆ (i : ι), (S i)⁻¹

@[simp]

theorem add_submonoid.neg_supr {G : Type u_2} [add_group G] {ι : Sort u_1} (S : ι → add_submonoid G) :

(-⨆ (i : ι), S i) = ⨆ (i : ι), -S i

@[protected]

def submonoid.pointwise_mul_action {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] [mul_distrib_mul_action α M] :

mul_action α (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.pointwise_mul_action = {to_has_smul := {smul := λ (a : α) (S : submonoid M), submonoid.map (⇑(mul_distrib_mul_action.to_monoid_End α M) a) S}, one_smul := _, mul_smul := _}

@[simp]

theorem submonoid.coe_pointwise_smul {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α M] (m : M) (a : α) (S : submonoid M) :

m ∈ a • S ↔ ∃ (s : M), s ∈ S ∧ a • s = m

@[simp]

theorem submonoid.smul_bot {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] [mul_distrib_mul_action α M] (a : α) :

a • ⊥ = ⊥

theorem submonoid.smul_sup {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α M] (a : α) (s : set M) :

a • submonoid.closure s = submonoid.closure (a • s)

@[protected, instance]

def submonoid.pointwise_central_scalar {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] [mul_distrib_mul_action α M] [mul_distrib_mul_action αᵐᵒᵖ M] [is_central_scalar α M] :

is_central_scalar α (submonoid M)

@[simp]

theorem submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [monoid M] [group α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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] [group_with_zero α] [mul_distrib_mul_action α 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] [group_with_zero α] [mul_distrib_mul_action α 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] [group_with_zero α] [mul_distrib_mul_action α 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] [group_with_zero α] [mul_distrib_mul_action α 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] [group_with_zero α] [mul_distrib_mul_action α 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] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a ≠ 0) {S T : submonoid M} :

S ≤ a • T ↔ a⁻¹ • S ≤ T

theorem add_submonoid.mem_closure_neg {G : Type u_1} [add_group G] (S : set G) (x : G) :

x ∈ add_submonoid.closure (-S) ↔ -x ∈ add_submonoid.closure S

theorem submonoid.mem_closure_inv {G : Type u_1} [group G] (S : set G) (x : G) :

x ∈ submonoid.closure S⁻¹ ↔ x⁻¹ ∈ submonoid.closure S

@[protected]

def add_submonoid.pointwise_mul_action {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] :

mul_action α (add_submonoid 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

add_submonoid.pointwise_mul_action = {to_has_smul := {smul := λ (a : α) (S : add_submonoid A), add_submonoid.map (⇑(distrib_mul_action.to_add_monoid_End α A) a) S}, one_smul := _, mul_smul := _}

@[simp]

theorem add_submonoid.coe_pointwise_smul {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] (a : α) (S : add_submonoid A) :

↑(a • S) = a • ↑S

theorem add_submonoid.smul_mem_pointwise_smul {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] (m : A) (a : α) (S : add_submonoid A) :

m ∈ S → a • m ∈ a • S

theorem add_submonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] (m : A) (a : α) (S : add_submonoid A) :

m ∈ a • S ↔ ∃ (s : A), s ∈ S ∧ a • s = m

@[simp]

theorem add_submonoid.smul_bot {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] (a : α) :

a • ⊥ = ⊥

theorem add_submonoid.smul_sup {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] (a : α) (S T : add_submonoid A) :

a • (S ⊔ T) = a • S ⊔ a • T

@[simp]

theorem add_submonoid.smul_closure {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] (a : α) (s : set A) :

a • add_submonoid.closure s = add_submonoid.closure (a • s)

@[protected, instance]

def add_submonoid.pointwise_central_scalar {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] [distrib_mul_action αᵐᵒᵖ A] [is_central_scalar α A] :

is_central_scalar α (add_submonoid A)

@[simp]

theorem add_submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S : add_submonoid A} {x : A} :

a • x ∈ a • S ↔ x ∈ S

theorem add_submonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {A : Type u_5} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S : add_submonoid A} {x : A} :

x ∈ a • S ↔ a⁻¹ • x ∈ S

theorem add_submonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S : add_submonoid A} {x : A} :

x ∈ a⁻¹ • S ↔ a • x ∈ S

@[simp]

theorem add_submonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S T : add_submonoid A} :

a • S ≤ a • T ↔ S ≤ T

theorem add_submonoid.pointwise_smul_le_iff {α : Type u_1} {A : Type u_5} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S T : add_submonoid A} :

a • S ≤ T ↔ S ≤ a⁻¹ • T

theorem add_submonoid.le_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S T : add_submonoid A} :

S ≤ a • T ↔ a⁻¹ • S ≤ T

@[simp]

theorem add_submonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) (S : add_submonoid A) (x : A) :

a • x ∈ a • S ↔ x ∈ S

theorem add_submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {A : Type u_5} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) (S : add_submonoid A) (x : A) :

x ∈ a • S ↔ a⁻¹ • x ∈ S

theorem add_submonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) (S : add_submonoid A) (x : A) :

x ∈ a⁻¹ • S ↔ a • x ∈ S

@[simp]

theorem add_submonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) {S T : add_submonoid A} :

a • S ≤ a • T ↔ S ≤ T

theorem add_submonoid.pointwise_smul_le_iff₀ {α : Type u_1} {A : Type u_5} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) {S T : add_submonoid A} :

a • S ≤ T ↔ S ≤ a⁻¹ • T

theorem add_submonoid.le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) {S T : add_submonoid 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.has_mul, as that API is usually more useful.

@[protected, instance]

def add_submonoid.has_one {R : Type u_4} [add_monoid_with_one R] :

has_one (add_submonoid R)

Equations

add_submonoid.has_one = {one := add_monoid_hom.mrange (nat.cast_add_monoid_hom R)}

theorem add_submonoid.one_eq_mrange {R : Type u_4} [add_monoid_with_one R] :

1 = add_monoid_hom.mrange (nat.cast_add_monoid_hom R)

theorem add_submonoid.nat_cast_mem_one {R : Type u_4} [add_monoid_with_one R] (n : ℕ) :

@[simp]

theorem add_submonoid.mem_one {R : Type u_4} [add_monoid_with_one R] {x : R} :

x ∈ 1 ↔ ∃ (n : ℕ), ↑n = x

theorem add_submonoid.one_eq_closure {R : Type u_4} [add_monoid_with_one R] :

1 = add_submonoid.closure {1}

theorem add_submonoid.one_eq_closure_one_set {R : Type u_4} [add_monoid_with_one R] :

1 = add_submonoid.closure 1

@[protected, instance]

def add_submonoid.has_mul {R : Type u_4} [non_unital_non_assoc_semiring R] :

has_mul (add_submonoid 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

add_submonoid.has_mul = {mul := λ (M N : add_submonoid R), ⨆ (s : ↥M), add_submonoid.map (⇑add_monoid_hom.mul s.val) N}

theorem add_submonoid.mul_mem_mul {R : Type u_4} [non_unital_non_assoc_semiring R] {M N : add_submonoid R} {m n : R} (hm : m ∈ M) (hn : n ∈ N) :

m * n ∈ M * N

theorem add_submonoid.mul_le {R : Type u_4} [non_unital_non_assoc_semiring R] {M N P : add_submonoid R} :

M * N ≤ P ↔ ∀ (m : R), m ∈ M → ∀ (n : R), n ∈ N → m * n ∈ P

@[protected]

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

C r

theorem add_submonoid.closure_mul_closure {R : Type u_4} [non_unital_non_assoc_semiring R] (S T : set R) :

add_submonoid.closure S * add_submonoid.closure T = add_submonoid.closure (S * T)

theorem add_submonoid.mul_eq_closure_mul_set {R : Type u_4} [non_unital_non_assoc_semiring R] (M N : add_submonoid R) :

M * N = add_submonoid.closure (↑M * ↑N)

@[simp]

theorem add_submonoid.mul_bot {R : Type u_4} [non_unital_non_assoc_semiring R] (S : add_submonoid R) :

@[simp]

theorem add_submonoid.bot_mul {R : Type u_4} [non_unital_non_assoc_semiring R] (S : add_submonoid R) :

theorem add_submonoid.mul_le_mul {R : Type u_4} [non_unital_non_assoc_semiring R] {M N P Q : add_submonoid R} (hmp : M ≤ P) (hnq : N ≤ Q) :

M * N ≤ P * Q

theorem add_submonoid.mul_le_mul_left {R : Type u_4} [non_unital_non_assoc_semiring R] {M N P : add_submonoid R} (h : M ≤ N) :

M * P ≤ N * P

theorem add_submonoid.mul_le_mul_right {R : Type u_4} [non_unital_non_assoc_semiring R] {M N P : add_submonoid R} (h : N ≤ P) :

M * N ≤ M * P

theorem add_submonoid.mul_subset_mul {R : Type u_4} [non_unital_non_assoc_semiring R] {M N : add_submonoid R} :

↑M * ↑N ⊆ ↑(M * N)

@[protected]

def add_submonoid.has_distrib_neg {R : Type u_4} [non_unital_non_assoc_ring R] :

has_distrib_neg (add_submonoid R)

add_submonoid.has_pointwise_neg distributes over multiplication.

This is available as an instance in the pointwise locale.

Equations

add_submonoid.has_distrib_neg = {neg := has_neg.neg (has_involutive_neg.to_has_neg (add_submonoid R)), neg_neg := _, neg_mul := _, mul_neg := _}

@[protected, instance]

def add_submonoid.mul_one_class {R : Type u_4} [non_assoc_semiring R] :

mul_one_class (add_submonoid R)

Equations

add_submonoid.mul_one_class = {one := 1, mul := has_mul.mul add_submonoid.has_mul, one_mul := _, mul_one := _}

@[protected, instance]

def add_submonoid.semigroup {R : Type u_4} [non_unital_semiring R] :

semigroup (add_submonoid R)

Equations

add_submonoid.semigroup = {mul := has_mul.mul add_submonoid.has_mul, mul_assoc := _}

@[protected, instance]

def add_submonoid.monoid {R : Type u_4} [semiring R] :

monoid (add_submonoid R)

Equations

add_submonoid.monoid = {mul := has_mul.mul add_submonoid.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (add_submonoid R)), npow_zero' := _, npow_succ' := _}

theorem add_submonoid.closure_pow {R : Type u_4} [semiring R] (s : set R) (n : ℕ) :

add_submonoid.closure s ^ n = add_submonoid.closure (s ^ n)

theorem add_submonoid.pow_eq_closure_pow_set {R : Type u_4} [semiring R] (s : add_submonoid R) (n : ℕ) :

s ^ n = add_submonoid.closure (↑s ^ n)

theorem add_submonoid.pow_subset_pow {R : Type u_4} [semiring R] {s : add_submonoid R} {n : ℕ} :

↑s ^ n ⊆ ↑(s ^ n)

theorem set.is_pwo.add_submonoid_closure {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : set α} (hpos : ∀ (x : α), x ∈ s → 0 ≤ x) (h : s.is_pwo) :

↑(add_submonoid.closure s).is_pwo

theorem set.is_pwo.submonoid_closure {α : Type u_1} [ordered_cancel_comm_monoid α] {s : set α} (hpos : ∀ (x : α), x ∈ s → 1 ≤ x) (h : s.is_pwo) :

↑(submonoid.closure s).is_pwo