map — Mathlib

English

If x and y commute in a monoid, then their images under any multiplicative homomorphism also commute: f(x) and f(y) commute.

Русский

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

LaTeX

$$$Commute(x,y) \Rightarrow Commute(f(x), f(y))$$$

Lean4

@[to_additive (attr := simp)]
protected theorem map [MulHomClass F M N] (h : Commute x y) (f : F) : Commute (f x) (f y) :=
  SemiconjBy.map h f

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