English
Equipping PreQuasiregular R with multiplication x*y = y + x + x*y (in the ambient ring R) yields a monoid with unit element corresponding to 0 under the canonical equivalence.
Русский
На множестве PreQuasiregular R вводим умножение x*y = y + x + x*y; получается моноид, единица соответствует 0 через каноническое эквивитивное отображение.
LaTeX
$$$$ (\text{PreQuasiregular}(R), \cdot) \text{ is a monoid with } x \cdot y = y + x + x y, \ 1 = \text{(image of 0)} $$$$
Lean4
instance instMonoid : Monoid (PreQuasiregular R) where
one := equiv 0
mul x y := .mk (y.val + x.val + x.val * y.val)
mul_one _ := equiv.symm.injective <| by simp [-EmbeddingLike.apply_eq_iff_eq]
one_mul _ := equiv.symm.injective <| by simp [-EmbeddingLike.apply_eq_iff_eq]
mul_assoc x y z := equiv.symm.injective <| by simp [mul_add, add_mul, mul_assoc]; abel
