English
If a and b are invertible in a Monoid α, then a b is invertible with inverse ⅟b * ⅟a, i.e., (a b)^{-1} = b^{-1} a^{-1}.
Русский
Если a и b обратимы в моноиде α, то произведение a b обратимо и имеет обратное ⅟b * ⅟a, то есть (a b)^{-1} = b^{-1} a^{-1}.
LaTeX
$$$\\forall a,b\\in\\alpha, \\text{Invertible } a, \\text{Invertible } b \\Rightarrow \\text{Invertible}(a b) \\,:\\, (a b)^{-1} = b^{-1} a^{-1}$$$
Lean4
/-- If `r` is invertible and `s = r` and `si = ⅟r`, then `s` is invertible with `⅟s = si`. -/
def copy' [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (si : α) (hs : s = r) (hsi : si = ⅟r) : Invertible s
where
invOf := si
invOf_mul_self := by rw [hs, hsi, invOf_mul_self]
mul_invOf_self := by rw [hs, hsi, mul_invOf_self]
