Theorem Projectivization.mulHeight_ne_zero

Modification history

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