Commit 2024-08-27 19:30 a8c57d86

View on Github →

chore(SetTheory/Ordinal/Exponential): use pow instead of opow (#16180) The theorem sup_opow_nat gets renamed in #15820, so I won't rename it here.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

added theorem Ordinal.opow_natCast

modified theorem Ordinal.sup_opow_nat

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean