mahlerMeasure_const

Mathlib.Analysis.Polynomial.MahlerMeasure

URI: https://scilib.ai/kg/mathlib#Polynomial.mahlerMeasure_const

← MathLib Explorer

English

The Mahler measure of a constant polynomial C z equals |z|.

Русский

Мера Малера константного многочлена C z равна |z|.

LaTeX

$$$$ \\mathrm{mahlerMeasure}(C z) = \\|z\\|. $$$$

Lean4

@[simp]
theorem mahlerMeasure_const (z : ℂ) : (C z).mahlerMeasure = ‖z‖ :=
  by
  simp only [mahlerMeasure, ne_eq, map_eq_zero, logMahlerMeasure_const, ite_not]
  split_ifs with h
  · simp [h]
  · simp [h, exp_log]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru