isConformalMap — Mathlib

English

If f' is a linear isometry from M to N, then f' is a conformal map; in particular the conformal factor is 1.

Русский

Если f' является линейной изометрией от пространства M к N, то она конформна; конформный множитель равен 1.

LaTeX

$$$IsConformalMap\ f'$, where $f' : M \to_L[R] N$ is a linear isometry.$$

Lean4

protected theorem isConformalMap (f' : M →ₗᵢ[R] N) : IsConformalMap f'.toContinuousLinearMap :=
  ⟨1, one_ne_zero, f', (one_smul _ _).symm⟩

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