normSq_neg

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.normSq_neg

English

normSq(-z) = normSq(z).

Русский

normSq(-z) = normSq(z).

LaTeX

$$$$\\operatorname{normSq}(-z) = \\operatorname{normSq}(z).$$$$

Lean4

@[simp, rclike_simps]
theorem normSq_neg (z : K) : normSq (-z) = normSq z := by simp only [normSq_eq_def', norm_neg]

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

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

Разделы

Аффилиация

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