inv_cpow_eq_ite' — Mathlib

English

An alternative formulation of inv_cpow_eq_ite with the ite placed on the other side, i.e., (x^n)⁻¹ equals a piecewise expression depending on x.arg.

Русский

Альтернативная формулировка inv_cpow_eq_ite с ite на другой стороне; то есть (x^n)⁻¹ выражается через разбиение по arg(x).

LaTeX

$$$(x^n)^{-1} = \begin{cases} conj(x^{-1})^{conj n} & \text{if } x.arg = \pi \\ x^{-1^n} & \text{otherwise} \end{cases}$$$

Lean4

/-- `Complex.inv_cpow_eq_ite` with the `ite` on the other side. -/
theorem inv_cpow_eq_ite' (x : ℂ) (n : ℂ) : (x ^ n)⁻¹ = if x.arg = π then conj (x⁻¹ ^ conj n) else x⁻¹ ^ n :=
  by
  rw [inv_cpow_eq_ite, apply_ite conj, conj_conj, conj_conj]
  split_ifs with h
  · rfl
  · rw [inv_cpow _ _ h]

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