normSq_inv

Mathlib.Analysis.RCLike.Basic

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

English

For any z ∈ K, normSq(z)^{-1} equals normSq(z^{-1}).

Русский

Для любого z ∈ K, (normSq(z))^{-1} = normSq(z^{-1}).

LaTeX

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

Lean4

@[rclike_simps]
theorem normSq_inv (z : K) : normSq z⁻¹ = (normSq z)⁻¹ :=
  map_inv₀ normSq z

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

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

Разделы

Аффилиация

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