normSq_div

Mathlib.Analysis.RCLike.Basic

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

English

For z,w ∈ K, normSq(z/w) = normSq(z) / normSq(w).

Русский

Для z,w ∈ K верно normSq(z/w) = normSq(z) / normSq(w).

LaTeX

$$$$ \operatorname{normSq}\left(\frac{z}{w}\right) = \frac{\operatorname{normSq}(z)}{\operatorname{normSq}(w)}. $$$$

Lean4

@[rclike_simps]
theorem normSq_div (z w : K) : normSq (z / w) = normSq z / normSq w :=
  map_div₀ normSq z w

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

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

Разделы

Аффилиация

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