coe_refl' — Mathlib

English

The underlying map of the identity equivalence equals the identity map.

Русский

Порождающее отображение тождественного эквивалентного отображения равно тождественному отображению.

LaTeX

$$$\uparrow(\text{ContinuousLinearEquiv.refl } R_1 M_1) = \text{ContinuousLinearMap.id } R_1 M_1$$$

Lean4

@[simp, norm_cast]
theorem coe_refl' : ⇑(ContinuousLinearEquiv.refl R₁ M₁) = id :=
  rfl

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