Commit 2024-10-11 19:55 2a154560

View on Github →

chore(SetTheory/Ordinal/Exponential): Ordinal.log cleanup (#17635) We do the following:

  • Make the definition of log a non-dependent if.
  • Private log_nonempty.
  • Deprecate log_of_not_one_lt_left in favor of log_of_left_le_one.
  • Remove an unnecessary argument from log_mod_opow_log_lt_log_self.
  • Drive-by proof cleanup.

Estimated changes

modified theorem Ordinal.log_def
modified theorem Ordinal.log_le_self
modified theorem Ordinal.log_mono_right
deleted theorem Ordinal.log_nonempty
modified theorem Ordinal.log_of_left_le_one
modified theorem Ordinal.log_one_right
modified theorem Ordinal.log_zero_right