mathlib3 documentation

group_theory.group_action.sub_mul_action.pointwise

Pointwise monoid structures on sub_mul_action #

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

This file provides sub_mul_action.monoid and weaker typeclasses, which show that sub_mul_actions inherit the same pointwise multiplications as sets.

To match submodule.idem_semiring, we do not put these in the pointwise locale.

@[protected, instance]
def sub_mul_action.has_one {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_one M] :
Equations
theorem sub_mul_action.coe_one {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_one M] :
1 = set.range (λ (r : R), r 1)
@[simp]
theorem sub_mul_action.mem_one {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_one M] {x : M} :
x 1 (r : R), r 1 = x
theorem sub_mul_action.subset_coe_one {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_one M] :
1 1
@[protected, instance]
def sub_mul_action.has_mul {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_mul M] [is_scalar_tower R M M] :
Equations
@[norm_cast]
theorem sub_mul_action.coe_mul {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_mul M] [is_scalar_tower R M M] (p q : sub_mul_action R M) :
(p * q) = p * q
theorem sub_mul_action.mem_mul {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_mul M] [is_scalar_tower R M M] {p q : sub_mul_action R M} {x : M} :
x p * q (y z : M), y p z q y * z = x
@[protected, instance]
def sub_mul_action.semigroup {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [semigroup M] [is_scalar_tower R M M] :
Equations
@[protected, instance]
def sub_mul_action.monoid {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [monoid M] [is_scalar_tower R M M] [smul_comm_class R M M] :
Equations
theorem sub_mul_action.coe_pow {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [monoid M] [is_scalar_tower R M M] [smul_comm_class R M M] (p : sub_mul_action R M) {n : } (hn : n 0) :
(p ^ n) = p ^ n
theorem sub_mul_action.subset_coe_pow {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [monoid M] [is_scalar_tower R M M] [smul_comm_class R M M] (p : sub_mul_action R M) {n : } :
p ^ n (p ^ n)