Theorem NumberField.logHeight₁_eq

Modification history

2026-03-02 16:30
Mathlib/NumberTheory/Height/NumberField.lean
feat(NumberTheory/Height): formula for logHeight₁ (#35919) …
Added NumberField.logHeight₁_eqView on Github →