coe_toAffineIsometry — Mathlib

English

The function underlying a linear isometry's affine version is exactly the original linear map.

Русский

Функция, лежащая в основе аффинного отображения линейной изометрии, равна исходному линейному отображению.

LaTeX

$$$\text{toAffineIsometry}(f): V \to P₂$ satisfies $\text{coe}(f.toAffineIsometry) = f$.$$

Lean4

@[simp]
theorem coe_toAffineIsometry : ⇑(f.toAffineIsometry : V →ᵃⁱ[𝕜] V₂) = f :=
  rfl

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