map_eq_one_iff — Mathlib

English

Let M and N be monoids and f: M → N be a monoid homomorphism which is injective. Then for every x in M, f(x) = 1 in N if and only if x = 1 in M.

Русский

Пусть M и N — моноиды, а f: M → N — моноид-гомоморфизм, инъективный. Тогда для каждого x ∈ M верно: f(x) = 1 в N тогда и только тогда x = 1 в M.

LaTeX

$$$\forall x \in M,\ f(x)=1 \iff x=1$$$

Lean4

@[to_additive]
theorem map_eq_one_iff [OneHomClass F M N] (f : F) (hf : Function.Injective f) {x : M} : f x = 1 ↔ x = 1 :=
  hf.eq_iff' (map_one f)

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