English
Unitization(R, A) is a monoid with respect to multiplication when R is a commutative monoid and A acts suitably.
Русский
Unitization(R, A) образует моноид относительно умножения при условии, что R — коммутативный моноид, и A удовлетворяет требованиям действия.
LaTeX
$$$\text{Monoid}(\mathrm{Unitization}(R,A))$$$
Lean4
instance instMonoid [CommMonoid R] [NonUnitalSemiring A] [DistribMulAction R A] [IsScalarTower R A A]
[SMulCommClass R A A] : Monoid (Unitization R A) :=
{ Unitization.instMulOneClass with
mul_assoc := fun x y z =>
ext (mul_assoc x.1 y.1 z.1) <|
show
(x.1 * y.1) • z.2 + z.1 • (x.1 • y.2 + y.1 • x.2 + x.2 * y.2) + (x.1 • y.2 + y.1 • x.2 + x.2 * y.2) * z.2 =
x.1 • (y.1 • z.2 + z.1 • y.2 + y.2 * z.2) + (y.1 * z.1) • x.2 + x.2 * (y.1 • z.2 + z.1 • y.2 + y.2 * z.2)
by
simp only [smul_add, mul_add, add_mul, smul_smul, smul_mul_assoc, mul_smul_comm, mul_assoc]
rw [mul_comm z.1 x.1]
rw [mul_comm z.1 y.1]
abel }
