Commit 2026-03-05 11:23 7b60111a

View on Github →

refactor: nicer definition for ordinal logarithm (#35850) By leveraging the API on Order.IsNormal, we can define the ordinal logarithm in a way that more immediately proves the characterizing Galois connection. Note that this removes Ordinal.log_def and Ordinal.succ_log_def without deprecation - these are auxiliary results that should have been private and are tedious to re-prove.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

modified theorem Ordinal.div_opow_log_lt

modified theorem Ordinal.div_opow_log_pos

modified def Ordinal.log

deleted theorem Ordinal.log_def

modified theorem Ordinal.log_of_left_le_one

modified theorem Ordinal.log_one_left

modified theorem Ordinal.log_zero_left

deleted theorem Ordinal.succ_log_def