instMulOneClass — Mathlib

English

SubMulAction R M forms a Semigroup under the multiplication defined by Set.image2 of multiplication.

Русский

SubMulAction R M образует полугруппу под действием умножения, заданного через образование Set.image2 умножения.

LaTeX

$$$\\text{SubMulAction }\\,R\\,M\\text{ is a Semigroup under }\\cdot.$$$

Lean4

instance : MulOneClass (SubMulAction R M) where
  mul := (· * ·)
  one := 1
  mul_one
    a := by
    ext x
    simp only [mem_mul, mem_one, mul_smul_comm, exists_exists_eq_and, mul_one]
    constructor
    · rintro ⟨y, hy, r, rfl⟩
      exact smul_mem _ _ hy
    · intro hx
      exact ⟨x, hx, 1, one_smul _ _⟩
  one_mul
    a := by
    ext x
    simp only [mem_mul, mem_one, smul_mul_assoc, exists_exists_eq_and, one_mul]
    refine ⟨?_, fun hx => ⟨1, x, hx, one_smul _ _⟩⟩
    rintro ⟨r, y, hy, rfl⟩
    exact smul_mem _ _ hy

Похожие утверждения