congr_arg — Mathlib

English

Let f be any multiplicative isomorphism between M and N. For all x, x' in M, if x = x' then f(x) = f(x'). In other words, a multiplicative isomorphism preserves equality of inputs.

Русский

Пусть f — мультипликативный изоморфизм между M и N. Для любых x, x' ∈ M верно: x = x' ⇒ f(x) = f(x'). Другими словами, отображение сохраняет равенство входов.

LaTeX

$$$\\forall f: M \\to N, \\forall x,x' \\in M, x = x' \\Rightarrow f(x) = f(x').$$$

Lean4

@[to_additive]
protected theorem congr_arg {f : MulEquiv M N} {x x' : M} : x = x' → f x = f x' :=
  DFunLike.congr_arg f

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