isLocalHom_of_leftInverse — Mathlib

English

If there exists a left inverse g for f, then f is a local homomorphism.

Русский

Если существует левый обратный g к f, то f является локальным гомоморфизмом.

LaTeX

$$$[\\text{FunLike } G S R] [\\text{MonoidHomClass } G S R] \\Rightarrow \\text{IsLocalHom}(f)$ given a left inverse g of f.$$

Lean4

theorem isLocalHom_of_leftInverse [FunLike G S R] [MonoidHomClass G S R] {f : F} (g : G)
    (hfg : Function.LeftInverse g f) : IsLocalHom f where
  map_nonunit a ha := by rwa [isUnit_map_of_leftInverse g hfg] at ha

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