ofEq_rfl — Mathlib

English

Special case: the identity isometry coming from the reflexive equality is the identity map.

Русский

Стандартный частный случай: изометрия, полученная из рефлексивного равенства, является тождественным отображением.

LaTeX

$$$\mathrm{ofEq}(\mathrm{rfl}) = \mathrm{id}_Q$$$

Lean4

@[simp]
theorem ofEq_rfl {Q : QuadraticMap R M₁ N} : ofEq (rfl : Q = Q) = .id Q :=
  rfl

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