English
Units α have a natural multiplication given by (u1 · u2). The underlying value satisfies (u1 · u2).val = u1.val · u2.val.
Русский
Единицы α имеют естественное умножение, задаваемое (u1 · u2).underlying; при этом (u1 · u2).val = u1.val · u2.val.
LaTeX
$$$$ (u_1 \\cdot u_2).\\text{val} = u_1.\\text{val} \\cdot u_2.\\text{val}. $$$$
Lean4
/-- Units of a monoid have an induced multiplication. -/
@[to_additive /-- Additive units of an additive monoid have an induced addition. -/
]
instance : Mul αˣ where
mul u₁
u₂ :=
⟨u₁.val * u₂.val, u₂.inv * u₁.inv, by rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv], by
rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]⟩
