Theorem Projectivization.logHeight_nonneg

Modification history

2026-02-18 07:51
Mathlib/NumberTheory/Height/Projectivization.lean
feat(NumberTheory/Height/Projectivization): new file (#34780) …
Added Projectivization.logHeight_nonnegView on Github →