map — Mathlib

English

If f is a local homomorphism and x is a unit in the domain, then f(x) is a unit in the codomain.

Русский

Пусть f — локальное гомоморфизм, и x — единица в области; тогда f(x) — единица в кодомене.

LaTeX

$$$\\text{IsUnit}(x) \\Rightarrow \\text{IsUnit}(f(x))$ for a local hom f.$$

Lean4

@[to_additive]
theorem map [MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x) : IsUnit (f x) := by rcases h with ⟨y, rfl⟩;
  exact (Units.map (f : M →* N) y).isUnit

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