arg_div_self — Mathlib

English

For every complex number x, the argument of x divided by itself is 0.

Русский

Для любого комплексного числа x аргумент частного x на x равен нулю.

LaTeX

$$$$ \arg\left(\frac{x}{x}\right) = 0, \quad x \in \mathbb{C}. $$$$

Lean4

/-- This holds true for all `x : ℂ` because of the junk values `0 / 0 = 0` and `arg 0 = 0`. -/
@[simp]
theorem arg_div_self (x : ℂ) : arg (x / x) = 0 := by obtain rfl | hx := eq_or_ne x 0 <;> simp [*]

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