map_id_apply — Mathlib

English

Applying the residue-field map to the identity ring homomorphism leaves residue-field elements fixed.

Русский

Применение отображения поля остатка к тождественному гомоморфизму кольца фиксирует элементы поля остатка.

LaTeX

$$$ \\operatorname{ResidueField.map} (\\mathrm{id} \\, R)\\; x = x $$$

Lean4

theorem map_id_apply (x : ResidueField R) : map (RingHom.id R) x = x :=
  DFunLike.congr_fun map_id x

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