linear_eq_linearIsometry — Mathlib

English

For every affine isometry f, the linear part equals the linear map underlying its linear isometry: f.linear = f.linearIsometry.toLinearMap.

Русский

Для каждой аффинной изометрии f линейная часть равна линейному отображению, лежащему в основе её линейной изометрии: f.linear = f.linearIsometry.toLinearMap.

LaTeX

$$$f.linear = f.linearIsometry.toLinearMap$$$

Lean4

@[simp]
theorem linear_eq_linearIsometry : f.linear = f.linearIsometry.toLinearMap :=
  by
  ext
  rfl

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