logMahlerMeasure_const — Mathlib

English

For any z ∈ ℂ, log Mahler measure of the constant polynomial C z is log |z|.

Русский

Для любой константы z логарифмическая мера Малера константного многочлена C z равна log|z|.

LaTeX

$$$$ (C z).logMahlerMeasure = \\log \\|z\\|. $$$$

Lean4

@[simp]
theorem logMahlerMeasure_const (z : ℂ) : (C z).logMahlerMeasure = log ‖z‖ := by
  simp [logMahlerMeasure_def, circleAverage_def, mul_assoc]

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