map_id — Mathlib

English

Mapping an intermediate field along the identity map leaves it unchanged: S.map(id) = S.

Русский

Перенос промежуточного поля по тождественному отображению не изменяет его: S.map(id) = S.

LaTeX

$$$ S.map(\\mathrm{id}_{K,L}) = S $$$

Lean4

/-- Mapping intermediate fields along the identity does not change them. -/
theorem map_id : S.map (AlgHom.id K L) = S :=
  SetLike.coe_injective <| Set.image_id _

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