English
For a given f in a suitable FunLike/MulEquivClass setting, there is an instance declaring f a local hom—i.e., it preserves nonunits in a precise sense, with map_nonunit given by simp.
Русский
Для данного f в рамках подходящих условий FunLike/MulEquivClass существует инстанс, утверждающий, что f является локальным гомоморфизмом, то есть сохраняет ненулевые элементы вне единицы в точном смысле (map_nonunit упрощается).
LaTeX
$$$IsLocalHom\\, f$ with $map\\_nonunit$ := by simp$$
Lean4
@[to_additive (attr := simp high)]
theorem isUnit_map : IsUnit (f x) ↔ IsUnit x
where
mp
hx := by
simpa using
hx.map <|
MonoidHom.mk ⟨EquivLike.inv f, EquivLike.injective f <| by simp⟩ fun x y ↦ EquivLike.injective f <| by simp
mpr := .map f
