isConformalMap_id

Mathlib.Analysis.Normed.Operator.Conformal

URI: https://scilib.ai/kg/mathlib#isConformalMap_id

English

Identity map is conformal.

Русский

Идентичное отображение конформно.

LaTeX

$$$\\mathrm{isConformalMap\_id} : \\mathrm{IsConformalMap}(\\mathrm{id})$$$

Lean4

theorem isConformalMap_id : IsConformalMap (.id R M) :=
  ⟨1, one_ne_zero, id, by simp⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru