congr_fun — Mathlib

English

If two multiplicative isomorphisms f and g: M ≃* N are equal, then for every x in M, f(x) = g(x).

Русский

Если два мультипликативных изоморфизма f и g: M ≃* N равны, то для любого элемента x ∈ M выполняется f(x) = g(x).

LaTeX

$$$f = g \\Rightarrow \\forall x \\in M,\\ f(x) = g(x).$$$

Lean4

@[to_additive]
protected theorem congr_fun {f g : MulEquiv M N} (h : f = g) (x : M) : f x = g x :=
  DFunLike.congr_fun h x

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