inv_def

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.inv_def

English

The same inverse formula is often used: z⁻¹ = conj(z) · (normSq(z))⁻¹.

Русский

Чаще всего используют обратную формулу: z⁻¹ = conj(z) · (normSq(z))⁻¹.

LaTeX

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

Lean4

theorem inv_def (z : ℂ) : z⁻¹ = conj z * ((normSq z)⁻¹ : ℝ) :=
  rfl

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

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

Разделы

Аффилиация

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