isUnit_map_of_leftInverse — Mathlib

English

For two classes of homomorphisms with a left inverse relation, IsUnit (f x) ⇔ IsUnit x for all x.

Русский

Для двух классов гомоморфизмов с отношением левого обратного выполняется IsUnit (f x) ⇔ IsUnit x для всех x.

LaTeX

$$$\\forall x, \\text{IsUnit}(f(x)) \\Leftrightarrow \\text{IsUnit}(x).$$$

Lean4

/-- Prefer `IsLocalHom.of_leftInverse`, but we can't get rid of this because of `ToAdditive`. -/
@[to_additive]
theorem _root_.isUnit_map_of_leftInverse [MonoidHomClass F M N] [MonoidHomClass G N M] {f : F} {x : M} (g : G)
    (hfg : Function.LeftInverse g f) : IsUnit (f x) ↔ IsUnit x :=
  ⟨of_leftInverse g hfg, map _⟩

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