map_mem_nonunits_iff — Mathlib

English

For a local homomorphism f, f(a) is a nonunit in β iff a is a nonunit in α.

Русский

Для локального гомоморфа f: f(a) не единица в β тогда и только тогда, когда a не единица в α.

LaTeX

$$f(a) \in nonunits(\beta) \iff a \in nonunits(\alpha)$$

Lean4

@[simp high] -- High priority shortcut lemma

theorem map_mem_nonunits_iff [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) [IsLocalHom f] (a) :
    f a ∈ nonunits β ↔ a ∈ nonunits α :=
  ⟨fun h ha => h <| ha.map f, fun h ha => h <| ha.of_map⟩

Похожие утверждения