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.

ink

instance SubMulAction.instOneSubMulActionToSMul {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] [inst : One M] : One (SubMulAction R M)

Equations

• One or more equations did not get rendered due to their size.

ink

theorem SubMulAction.coe_one {R : Type u_2} {M : Type u_1} [inst : Monoid R] [inst : MulAction R M] [inst : One M] : ↑1 = Set.range fun r => r • 1

ink

@[simp]

theorem SubMulAction.mem_one {R : Type u_2} {M : Type u_1} [inst : Monoid R] [inst : MulAction R M] [inst : One M] {x : M} : x ∈ 1 ↔ ∃ r, r • 1 = x

ink

theorem SubMulAction.subset_coe_one {R : Type u_2} {M : Type u_1} [inst : Monoid R] [inst : MulAction R M] [inst : One M] : 1 ⊆ ↑1

ink

instance SubMulAction.instMulSubMulActionToSMul {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] [inst : Mul M] [inst : IsScalarTower R M M] : Mul (SubMulAction R M)

Equations

• One or more equations did not get rendered due to their size.

ink

theorem SubMulAction.coe_mul {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] [inst : Mul M] [inst : IsScalarTower R M M] (p : SubMulAction R M) (q : SubMulAction R M) : ↑(p * q) = ↑p * ↑q

ink

theorem SubMulAction.mem_mul {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] [inst : Mul M] [inst : IsScalarTower R M M] {p : SubMulAction R M} {q : SubMulAction R M} {x : M} : x ∈ p * q ↔ ∃ y z, y ∈ p ∧ z ∈ q ∧ y * z = x

ink

instance SubMulAction.mulOneClass {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] [inst : MulOneClass M] [inst : IsScalarTower R M M] [inst : SMulCommClass R M M] : MulOneClass (SubMulAction R M)

Equations

• SubMulAction.mulOneClass = MulOneClass.mk (_ : ∀ (a : SubMulAction R M), 1 * a = a) (_ : ∀ (a : SubMulAction R M), a * 1 = a)

ink

instance SubMulAction.semiGroup {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] [inst : Semigroup M] [inst : IsScalarTower R M M] : Semigroup (SubMulAction R M)

Equations

• SubMulAction.semiGroup = Semigroup.mk (_ : ∀ (x x_1 x_2 : SubMulAction R M), x * x_1 * x_2 = x * (x_1 * x_2))

ink

instance SubMulAction.instMonoidSubMulActionToSMul {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] [inst : Monoid M] [inst : IsScalarTower R M M] [inst : SMulCommClass R M M] : Monoid (SubMulAction R M)

Equations

• One or more equations did not get rendered due to their size.

ink

theorem SubMulAction.coe_pow {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] [inst : Monoid M] [inst : IsScalarTower R M M] [inst : SMulCommClass R M M] (p : SubMulAction R M) {n : ℕ} : n ≠ 0 → ↑(p ^ n) = ↑p ^ n

ink

theorem SubMulAction.subset_coe_pow {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] [inst : Monoid M] [inst : IsScalarTower R M M] [inst : SMulCommClass R M M] (p : SubMulAction R M) {n : ℕ} : ↑p ^ n ⊆ ↑(p ^ n)