normSq_mul

Mathlib.Analysis.RCLike.Basic

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

English

normSq(z w) = normSq(z) normSq(w).

Русский

normSq(z w) = normSq(z) \\cdot normSq(w).

LaTeX

$$$$\\operatorname{normSq}(z w) = \\operatorname{normSq}(z) \\cdot \\operatorname{normSq}(w).$$$$

Lean4

@[rclike_simps]
theorem normSq_mul (z w : K) : normSq (z * w) = normSq z * normSq w :=
  map_mul _ z w

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

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

Разделы

Аффилиация

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