Theorem Ordinal.nmul_le_nmul_left

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_left View on Github →