map_mul_eq_one — Mathlib

English

Let M,N be monoids and f a monoid homomorphism M → N. If a,b ∈ M satisfy a b = 1, then f(a) f(b) = 1 in N.

Русский

Пусть M, N — моноиды и f: M →* N — моноидный гомоморфизм. Пусть a,b ∈ M удовлетворяют a b = 1; тогда f(a) f(b) = 1 в N.

LaTeX

$$$$ \forall f: M \to^* N,\ \forall a,b \in M,\ a b = 1 \Rightarrow f(a) f(b) = 1. $$$$

Lean4

@[to_additive]
theorem map_mul_eq_one [MonoidHomClass F M N] (f : F) {a b : M} (h : a * b = 1) : f a * f b = 1 := by
  rw [← map_mul, h, map_one]

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