Theorem Projectivization.logHeight_eq_log_mulHeight

Modification history

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