Theorem Projectivization.one_le_mulHeight

Modification history

2026-02-18 07:51

Mathlib/NumberTheory/Height/Projectivization.lean

feat(NumberTheory/Height/Projectivization): new file (#34780) …

Added Projectivization.one_le_mulHeight View on Github →