kahler_apply_self

Mathlib.Analysis.InnerProductSpace.TwoDim

URI: https://scilib.ai/kg/mathlib#Orientation.kahler_apply_self

English

The self-evaluation of kahler matches the squared norm: kahler x x = ||x||^2.

Русский

Значение kahler на одинаковых аргументах равно квадрату нормы: kahler x x = ||x||^2.

LaTeX

$$kahler\\_apply\\_self (x) : o.kahler x x = ||x||^2$$

Lean4

@[simp]
theorem kahler_apply_self (x : E) : o.kahler x x = ‖x‖ ^ 2 := by simp [kahler_apply_apply, real_inner_self_eq_norm_sq]

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

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

Разделы

Аффилиация

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