map_id — Mathlib

English

Mapping by the identity star-algebra homomorphism leaves the subalgebra unchanged: S.map id = S.

Русский

Отображение по тождественной звездной алгоморфизмы оставляет подалгебру без изменений: S.map id = S.

LaTeX

$$$S.map\, (\mathrm{StarAlgHom.id}\; R\; A) = S$$$

Lean4

@[simp]
theorem map_id (S : StarSubalgebra R A) : S.map (StarAlgHom.id R A) = S :=
  SetLike.coe_injective <| Set.image_id _

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