toAffineIsometryEquiv_toAffineIsometry

English

The mapping from a LinearIsometryEquiv to its affine counterpart is the identity on the underlying function.

Русский

Переобразование LinearIsometryEquiv к аффинной форме не изменяет базовую функцию.

LaTeX

$$$$ \mathrm{coe\_to\_AffineIsometryEquiv}(e) = e^{\mathrm{toAffineIsometryEquiv}} $$$$

Lean4

@[simp]
theorem toAffineIsometryEquiv_toAffineIsometry :
    e.toAffineIsometryEquiv.toAffineIsometry = e.toLinearIsometry.toAffineIsometry :=
  rfl

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