map_id — Mathlib

English

Applying QuotSMulTop map to an identity map yields the identity on quotients.

Русский

Применение отображения QuotSMulTop к тождественному отображению дает тождественное отображение на частях.

LaTeX

$$$$ map\_r(\mathrm{id}_M) = \mathrm{id}_{QuotSMulTop(r,M)}. $$$$

Lean4

@[simp]
theorem map_id : map r (LinearMap.id : M →ₗ[R] M) = .id :=
  DFunLike.ext _ _ <| (mkQ_surjective _).forall.mpr fun _ => rfl

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