map_mul — Mathlib

English

A multiplicative isomorphism f preserves multiplication: f(xy) = f(x) f(y) for all x,y.

Русский

Мультипликативный изоморфизм f сохраняет умножение: f(xy) = f(x) f(y) для любых x,y.

LaTeX

$$$\\forall x,y,\\ f(xy)=f(x)f(y)$$$

Lean4

/-- A multiplicative isomorphism preserves multiplication. -/
@[to_additive /-- An additive isomorphism preserves addition. -/
    ]
protected theorem map_mul (f : M ≃* N) : ∀ x y, f (x * y) = f x * f y :=
  map_mul f

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