map — Mathlib

English

If a x = y a and f is a homomorphism, then f(a) f(x) = f(y) f(a). In other words, a semiconjugacy is preserved by any multiplicative homomorphism.

Русский

Если a x = y a и f — гомоморфизм умножения, то f(a) f(x) = f(y) f(a). Иными словами, полусопряжение сохраняется под любым умножающим гомоморфизмом.

LaTeX

$$$SemiconjBy\ a\ x\ y \Rightarrow SemiconjBy\ (f\,a)\ (f\,x)\ (f\,y)$$$

Lean4

@[to_additive (attr := simp)]
protected theorem map [MulHomClass F M N] (h : SemiconjBy a x y) (f : F) : SemiconjBy (f a) (f x) (f y) := by
  simpa only [SemiconjBy, map_mul] using congr_arg f h

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