Documentation

Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Pointwise monoid structures on SubMulAction #

This file provides SubMulAction.Monoid and weaker typeclasses, which show that SubMulActions inherit the same pointwise multiplications as sets.

To match Submodule.idemSemiring, we do not put these in the Pointwise locale.

instance SubMulAction.instOne {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] :
Equations
  • SubMulAction.instOne = { one := { carrier := Set.range fun (r : R) => r 1, smul_mem' := } }
theorem SubMulAction.coe_one {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] :
1 = Set.range fun (r : R) => r 1
@[simp]
theorem SubMulAction.mem_one {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] {x : M} :
x 1 ∃ (r : R), r 1 = x
theorem SubMulAction.subset_coe_one {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] :
1 1
instance SubMulAction.instMul {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Mul M] [IsScalarTower R M M] :
Equations
  • SubMulAction.instMul = { mul := fun (p q : SubMulAction R M) => { carrier := Set.image2 (fun (x1 x2 : M) => x1 * x2) p q, smul_mem' := } }
theorem SubMulAction.coe_mul {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Mul M] [IsScalarTower R M M] (p : SubMulAction R M) (q : SubMulAction R M) :
(p * q) = p * q
theorem SubMulAction.mem_mul {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Mul M] [IsScalarTower R M M] {p : SubMulAction R M} {q : SubMulAction R M} {x : M} :
x p * q yp, zq, y * z = x
instance SubMulAction.mulOneClass {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [MulOneClass M] [IsScalarTower R M M] [SMulCommClass R M M] :
Equations
instance SubMulAction.semiGroup {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Semigroup M] [IsScalarTower R M M] :
Equations
instance SubMulAction.instMonoid {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Monoid M] [IsScalarTower R M M] [SMulCommClass R M M] :
Equations
  • SubMulAction.instMonoid = Monoid.mk npowRec
theorem SubMulAction.coe_pow {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Monoid M] [IsScalarTower R M M] [SMulCommClass R M M] (p : SubMulAction R M) {n : } :
n 0(p ^ n) = p ^ n
theorem SubMulAction.subset_coe_pow {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Monoid M] [IsScalarTower R M M] [SMulCommClass R M M] (p : SubMulAction R M) {n : } :
p ^ n (p ^ n)