Commit 2024-09-12 05:45 05bd9c4e

View on Github →

chore(SetTheory/Ordinal/Arithmetic): hide implementation details (#16703) We private some lemmas which expose implementation details of functions.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.div_def

deleted theorem Ordinal.div_nonempty

deleted theorem Ordinal.sub_nonempty

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

deleted theorem Ordinal.nmul_nonempty