mathlib3 documentation

ring_theory.subsemiring.pointwise

Pointwise instances on subsemirings #

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

This file provides the action subsemiring.pointwise_mul_action which matches the action of mul_action_set.

This actions is available in the pointwise locale.

Implementation notes #

This file is almost identical to group_theory/submonoid/pointwise.lean. Where possible, try to keep them in sync.

@[protected]

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

This is available as an instance in the pointwise locale.

Equations
@[simp]
theorem subsemiring.coe_pointwise_smul {M : Type u_1} {R : Type u_2} [monoid M] [semiring R] [mul_semiring_action M R] (m : M) (S : subsemiring R) :
(m S) = m S
theorem subsemiring.smul_mem_pointwise_smul {M : Type u_1} {R : Type u_2} [monoid M] [semiring R] [mul_semiring_action M R] (m : M) (r : R) (S : subsemiring R) :
r S m r m S
theorem subsemiring.mem_smul_pointwise_iff_exists {M : Type u_1} {R : Type u_2} [monoid M] [semiring R] [mul_semiring_action M R] (m : M) (r : R) (S : subsemiring R) :
r m S (s : R), s S m s = r
@[simp]
theorem subsemiring.smul_bot {M : Type u_1} {R : Type u_2} [monoid M] [semiring R] [mul_semiring_action M R] (a : M) :
theorem subsemiring.smul_sup {M : Type u_1} {R : Type u_2} [monoid M] [semiring R] [mul_semiring_action M R] (a : M) (S T : subsemiring R) :
a (S T) = a S a T
theorem subsemiring.smul_closure {M : Type u_1} {R : Type u_2} [monoid M] [semiring R] [mul_semiring_action M R] (a : M) (s : set R) :
@[simp]
theorem subsemiring.smul_mem_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [group M] [semiring R] [mul_semiring_action M R] {a : M} {S : subsemiring R} {x : R} :
a x a S x S
theorem subsemiring.mem_pointwise_smul_iff_inv_smul_mem {M : Type u_1} {R : Type u_2} [group M] [semiring R] [mul_semiring_action M R] {a : M} {S : subsemiring R} {x : R} :
x a S a⁻¹ x S
theorem subsemiring.mem_inv_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [group M] [semiring R] [mul_semiring_action M R] {a : M} {S : subsemiring R} {x : R} :
x a⁻¹ S a x S
@[simp]
theorem subsemiring.pointwise_smul_le_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [group M] [semiring R] [mul_semiring_action M R] {a : M} {S T : subsemiring R} :
a S a T S T
theorem subsemiring.pointwise_smul_subset_iff {M : Type u_1} {R : Type u_2} [group M] [semiring R] [mul_semiring_action M R] {a : M} {S T : subsemiring R} :
a S T S a⁻¹ T
theorem subsemiring.subset_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [group M] [semiring R] [mul_semiring_action M R] {a : M} {S T : subsemiring R} :
S a T a⁻¹ S T

TODO: add equiv_smul like we have for subgroup.

@[simp]
theorem subsemiring.smul_mem_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [group_with_zero M] [semiring R] [mul_semiring_action M R] {a : M} (ha : a 0) (S : subsemiring R) (x : R) :
a x a S x S
theorem subsemiring.mem_pointwise_smul_iff_inv_smul_mem₀ {M : Type u_1} {R : Type u_2} [group_with_zero M] [semiring R] [mul_semiring_action M R] {a : M} (ha : a 0) (S : subsemiring R) (x : R) :
x a S a⁻¹ x S
theorem subsemiring.mem_inv_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [group_with_zero M] [semiring R] [mul_semiring_action M R] {a : M} (ha : a 0) (S : subsemiring R) (x : R) :
x a⁻¹ S a x S
@[simp]
theorem subsemiring.pointwise_smul_le_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [group_with_zero M] [semiring R] [mul_semiring_action M R] {a : M} (ha : a 0) {S T : subsemiring R} :
a S a T S T
theorem subsemiring.pointwise_smul_le_iff₀ {M : Type u_1} {R : Type u_2} [group_with_zero M] [semiring R] [mul_semiring_action M R] {a : M} (ha : a 0) {S T : subsemiring R} :
a S T S a⁻¹ T
theorem subsemiring.le_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [group_with_zero M] [semiring R] [mul_semiring_action M R] {a : M} (ha : a 0) {S T : subsemiring R} :
S a T a⁻¹ S T