mul_inv_cancel

Mathlib.Data.Complex.Basic

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

← MathLib Explorer

English

For z ∈ ℂ with z ≠ 0, z · z⁻¹ = 1.

Русский

Для z ∈ ℂ при z ≠ 0 выполняется z · z⁻¹ = 1.

LaTeX

$$$$z \neq 0 \Rightarrow z \cdot z^{-1} = 1.$$$$

Lean4

protected theorem mul_inv_cancel {z : ℂ} (h : z ≠ 0) : z * z⁻¹ = 1 := by
  rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel₀ (mt normSq_eq_zero.1 h), ofReal_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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