of_map — Mathlib

English

If f is a local hom and f(x) is irreducible, then x is irreducible.

Русский

Если f — локальная гомоморфия и f(x) неразложимо, то x неразложим.

LaTeX

$$$\\\\forall {F M N} [Monoid M] [Monoid N] [FunLike F M N] [MonoidHomClass F M N] [IsLocalHom f], \\\\mathrm{Irreducible} (f x) \\\\Rightarrow \\\\mathrm{Irreducible} x$$$

Lean4

theorem of_map [FunLike F M N] [MonoidHomClass F M N] [IsLocalHom f] (hfx : Irreducible (f x)) : Irreducible x
    where
  not_isUnit hu := hfx.not_isUnit <| hu.map f
  isUnit_or_isUnit := by rintro p q rfl; exact (hfx.isUnit_or_isUnit <| map_mul f p q).imp (.of_map f _) (.of_map f _)

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