coe_map — Mathlib

English

The map on unitary subgroups commutes with the underlying coercions: applying map to a unitary element yields the same result as mapping its representative.

Русский

Отображение на подгруппах унитарных элементов согласуется с базовыми коэрценциями: применение отображения к унитарному элементу равно отображению его представителей.

LaTeX

$$$ map f\\, x = f(x) \\quad (x \\in \\mathrm{unitary}(R))$$$

Lean4

@[simp]
theorem coe_map (f : R →⋆* S) (x : unitary R) : map f x = f x :=
  rfl

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