Commit 2023-11-16 23:07 c81061b3

feat: add lemmas on Complex.arg (x * y) and Complex.log (x * y) (#8346) This adds lemmas as in the title (plus one for arg (x * r) with real r):

lemma arg_mul_eq_add_arg_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
    (x * y).arg = x.arg + y.arg ↔ arg x + arg y ∈ Set.Ioc (-π) π
lemma arg_mul {x y : ℂ} (hx₀ : x ≠ 0) (hx₁ : -π / 2 < x.arg) (hx₂ : x.arg ≤ π / 2)
    (hy₀ : y ≠ 0) (hy₁ : -π / 2 < y.arg) (hy₂ : y.arg ≤ π / 2) :
    (x * y).arg = x.arg + y.arg
lemma log_mul_eq_add_log_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
    log (x * y) = log x + log y ↔ arg x + arg y ∈ Set.Ioc (-π) π
lemma log_mul {x y : ℂ} (hx₀ : x ≠ 0) (hx₁ : -π / 2 < x.arg) (hx₂ : x.arg ≤ π / 2)
    (hy₀ : y ≠ 0) (hy₁ : -π / 2 < y.arg) (hy₂ : y.arg ≤ π / 2) :
    (x * y).log = x.log + y.log

See here on Zulip.