logMahlerMeasure_mul_eq_add_logMahelerMeasure

English

If p,q ∈ ℂ[X] and pq ≠ 0, then log Mahler measure is additive: logM(pq) = logM(p) + logM(q).

Русский

Если p,q ∈ ℂ[X] и pq ≠ 0, тогда logM(pq) = logM(p) + logM(q).

LaTeX

$$$$ (p q).logMahlerMeasure = p.logMahlerMeasure + q.logMahlerMeasure \\quad \\text{if } p q \\neq 0. $$$$

Lean4

theorem logMahlerMeasure_mul_eq_add_logMahelerMeasure {p q : ℂ[X]} (hpq : p * q ≠ 0) :
    (p * q).logMahlerMeasure = p.logMahlerMeasure + q.logMahlerMeasure := by
  simp_all [logMahlerMeasure_eq_log_MahlerMeasure, mahlerMeasure_mul, log_mul]

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