Documentation

Mathlib.Algebra.Ring.Subring.Pointwise

Pointwise instances on Subrings #

This file provides the action Subring.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.Ring.Subsemiring.Pointwise. Where possible, try to keep them in sync.

def Subring.pointwiseMulAction {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] :

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

This is available as an instance in the Pointwise locale.

Equations
theorem Subring.pointwise_smul_def {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] {a : M} (S : Subring R) :
@[simp]
theorem Subring.coe_pointwise_smul {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (m : M) (S : Subring R) :
(m S) = m S
@[simp]
theorem Subring.pointwise_smul_toAddSubgroup {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (m : M) (S : Subring R) :
(m S).toAddSubgroup = m S.toAddSubgroup
@[simp]
theorem Subring.pointwise_smul_toSubsemiring {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (m : M) (S : Subring R) :
(m S).toSubsemiring = m S.toSubsemiring
theorem Subring.smul_mem_pointwise_smul {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (m : M) (r : R) (S : Subring R) :
r Sm r m S
instance Subring.instCovariantClassHSMulLe {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] :
CovariantClass M (Subring R) HSMul.hSMul LE.le
Equations
  • =
theorem Subring.mem_smul_pointwise_iff_exists {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (m : M) (r : R) (S : Subring R) :
r m S sS, m s = r
@[simp]
theorem Subring.smul_bot {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (a : M) :
theorem Subring.smul_sup {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (a : M) (S : Subring R) (T : Subring R) :
a (S T) = a S a T
theorem Subring.smul_closure {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (a : M) (s : Set R) :
@[simp]
theorem Subring.smul_mem_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Ring R] [MulSemiringAction M R] {a : M} {S : Subring R} {x : R} :
a x a S x S
theorem Subring.mem_pointwise_smul_iff_inv_smul_mem {M : Type u_1} {R : Type u_2} [Group M] [Ring R] [MulSemiringAction M R] {a : M} {S : Subring R} {x : R} :
x a S a⁻¹ x S
theorem Subring.mem_inv_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Ring R] [MulSemiringAction M R] {a : M} {S : Subring R} {x : R} :
x a⁻¹ S a x S
@[simp]
theorem Subring.pointwise_smul_le_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Ring R] [MulSemiringAction M R] {a : M} {S : Subring R} {T : Subring R} :
a S a T S T
theorem Subring.pointwise_smul_subset_iff {M : Type u_1} {R : Type u_2} [Group M] [Ring R] [MulSemiringAction M R] {a : M} {S : Subring R} {T : Subring R} :
a S T S a⁻¹ T
theorem Subring.subset_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Ring R] [MulSemiringAction M R] {a : M} {S : Subring R} {T : Subring R} :
S a T a⁻¹ S T

TODO: add equivSMul like we have for subgroup.

@[simp]
theorem Subring.smul_mem_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Ring R] [MulSemiringAction M R] {a : M} (ha : a 0) (S : Subring R) (x : R) :
a x a S x S
theorem Subring.mem_pointwise_smul_iff_inv_smul_mem₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Ring R] [MulSemiringAction M R] {a : M} (ha : a 0) (S : Subring R) (x : R) :
x a S a⁻¹ x S
theorem Subring.mem_inv_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Ring R] [MulSemiringAction M R] {a : M} (ha : a 0) (S : Subring R) (x : R) :
x a⁻¹ S a x S
@[simp]
theorem Subring.pointwise_smul_le_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Ring R] [MulSemiringAction M R] {a : M} (ha : a 0) {S : Subring R} {T : Subring R} :
a S a T S T
theorem Subring.pointwise_smul_le_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Ring R] [MulSemiringAction M R] {a : M} (ha : a 0) {S : Subring R} {T : Subring R} :
a S T S a⁻¹ T
theorem Subring.le_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Ring R] [MulSemiringAction M R] {a : M} (ha : a 0) {S : Subring R} {T : Subring R} :
S a T a⁻¹ S T