Documentation

Mathlib.Algebra.Ring.Subsemiring.Pointwise

Pointwise instances on Subsemirings #

This file provides the action Subsemiring.PointwiseMulAction which matches the action of MulActionSet.

This actions is available in the Pointwise locale.

Implementation notes #

This file is almost identical to the file Mathlib.Algebra.Group.Submonoid.Pointwise. Where possible, try to keep them in sync.

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

This is available as an instance in the Pointwise locale.

Equations
Instances For
    @[simp]
    theorem Subsemiring.coe_pointwise_smul {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (m : M) (S : Subsemiring R) :
    (m S) = m S
    @[simp]
    theorem Subsemiring.pointwise_smul_toAddSubmonoid {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (m : M) (S : Subsemiring R) :
    (m S).toAddSubmonoid = m S.toAddSubmonoid
    theorem Subsemiring.smul_mem_pointwise_smul {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (m : M) (r : R) (S : Subsemiring R) :
    r Sm r m S
    instance Subsemiring.instCovariantClassHSMulLe {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] :
    CovariantClass M (Subsemiring R) HSMul.hSMul LE.le
    Equations
    • =
    theorem Subsemiring.mem_smul_pointwise_iff_exists {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (m : M) (r : R) (S : Subsemiring R) :
    r m S sS, m s = r
    @[simp]
    theorem Subsemiring.smul_bot {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (a : M) :
    theorem Subsemiring.smul_sup {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (a : M) (S : Subsemiring R) (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] [MulSemiringAction 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] [MulSemiringAction 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] [MulSemiringAction 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] [MulSemiringAction 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] [MulSemiringAction M R] {a : M} {S : Subsemiring R} {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] [MulSemiringAction M R] {a : M} {S : Subsemiring R} {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] [MulSemiringAction M R] {a : M} {S : Subsemiring R} {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} [GroupWithZero M] [Semiring R] [MulSemiringAction 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} [GroupWithZero M] [Semiring R] [MulSemiringAction 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} [GroupWithZero M] [Semiring R] [MulSemiringAction 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} [GroupWithZero M] [Semiring R] [MulSemiringAction M R] {a : M} (ha : a 0) {S : Subsemiring R} {T : Subsemiring R} :
    a S a T S T
    theorem Subsemiring.pointwise_smul_le_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Semiring R] [MulSemiringAction M R] {a : M} (ha : a 0) {S : Subsemiring R} {T : Subsemiring R} :
    a S T S a⁻¹ T
    theorem Subsemiring.le_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Semiring R] [MulSemiringAction M R] {a : M} (ha : a 0) {S : Subsemiring R} {T : Subsemiring R} :
    S a T a⁻¹ S T