logMahlerMeasure_monomial — Mathlib

English

For monomial p(X) = z X^n, log Mahler measure equals log |z|, independent of n.

Русский

Для мономиала p(X) = z X^n логарифмическая мера Малера равна log|z|, независимо от n.

LaTeX

$$$$ (\\mathrm{monomial}\\ n\ z).logMahlerMeasure = \\log \\|z\\|. $$$$

Lean4

@[simp]
theorem logMahlerMeasure_monomial (n : ℕ) (z : ℂ) : (monomial n z).logMahlerMeasure = log ‖z‖ := by
  simp [logMahlerMeasure_def, circleAverage_def, mul_assoc]

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