norm_symm

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

URI: https://scilib.ai/kg/mathlib#EisensteinSeries.norm_symm

English

Identity of norms under permutation of coordinates in the same two-entry vector.

Русский

Идентичность нормы при перестановке координат в том же векторе из двух компонент.

LaTeX

$$‖![x,y]‖ = ‖![y,x]‖$$

Lean4

theorem norm_symm (x y : ℤ) : ‖![x, y]‖ = ‖![y, x]‖ := by simp [EisensteinSeries.norm_eq_max_natAbs, max_comm]

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

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

Разделы

Аффилиация

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