Theorem Ordinal.nmul_zero

Modification history

2025-11-24 09:57
Mathlib/SetTheory/Ordinal/NaturalOps.lean
chore: golf proofs that use `0 < x ↔ x ≠ 0` (#31895) …
Modified Ordinal.nmul_zeroView on Github →
2023-07-18 05:18
Mathlib/SetTheory/Ordinal/NaturalOps.lean
chore: forward port #14324 (#5973) …
Added Ordinal.nmul_zeroView on Github →