English
For monoid-like structures, if r is invertible and f is a homomorphism, then f(r^{-1}) = (f(r))^{-1} provided f(r) is invertible.
Русский
Пусть f — гомоморфизм моноидов. Если r обратим и f(r) обратимо, то f(r^{-1}) = (f(r))^{-1}.
LaTeX
$$$f(r)^{-1} = f(r^{-1})$$$
Lean4
/-- Note that the `Invertible (f r)` argument can be satisfied by using `letI := Invertible.map f r`
before applying this lemma. -/
theorem map_invOf {R : Type*} {S : Type*} {F : Type*} [MulOneClass R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S]
(f : F) (r : R) [Invertible r] [ifr : Invertible (f r)] : f (⅟r) = ⅟(f r) :=
have h : ifr = Invertible.map f r := Subsingleton.elim _ _
by subst h; rfl
