isConformalMap_const_smul

Mathlib.Analysis.Normed.Operator.Conformal

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

English

The constant scalar multiple of the identity is conformal when the scalar is nonzero.

Русский

Постоянное ненулевое умножение на единичное отображение конформно.

LaTeX

$$$\\mathrm{isConformalMap\_const\\_smul} (hc : c \\neq 0) : \\mathrm{IsConformalMap}(c \\cdot \\mathrm{\\id})$$$

Lean4

theorem isConformalMap_const_smul (hc : c ≠ 0) : IsConformalMap (c • .id R M) :=
  isConformalMap_id.smul hc

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

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

Разделы

Аффилиация

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