Theorem Height.logHeight₁_eq

Modification history

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