Theorem Ordinal.nmul_le_nmul_right

Modification history

2024-08-27 20:26

Mathlib/SetTheory/Ordinal/NaturalOps.lean

feat(SetTheory/Ordinal/NaturalOps): fix bad names (#15992) …

Added Ordinal.nmul_le_nmul_right View on Github →