Commit 2024-11-12 10:47 94c3588e

View on Github →

chore(SetTheory/Ordinal/Principal): use variable (#18898) ...plus a simple golf for isLimit_of_principal_add.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Principal.lean

modified theorem Ordinal.Principal.iterate_lt

modified theorem Ordinal.add_absorp

modified theorem Ordinal.add_omega0

modified theorem Ordinal.add_omega0_opow

modified theorem Ordinal.exists_lt_add_of_not_principal_add

modified theorem Ordinal.isLimit_of_principal_add

modified theorem Ordinal.isLimit_of_principal_mul

modified theorem Ordinal.mul_eq_opow_log_succ

modified theorem Ordinal.mul_lt_omega0_opow

modified theorem Ordinal.mul_omega0

modified theorem Ordinal.mul_omega0_dvd

modified theorem Ordinal.mul_omega0_opow_opow

modified theorem Ordinal.nfp_le_of_principal

modified theorem Ordinal.not_principal_iff

modified theorem Ordinal.op_eq_self_of_principal

modified theorem Ordinal.opow_omega0

modified theorem Ordinal.principal_add_iff_add_left_eq_self

modified theorem Ordinal.principal_add_iff_add_lt_ne_self

modified theorem Ordinal.principal_add_iff_zero_or_omega0_opow

modified theorem Ordinal.principal_add_of_le_one

modified theorem Ordinal.principal_add_of_principal_mul

modified theorem Ordinal.principal_add_of_principal_mul_opow

modified theorem Ordinal.principal_iff_of_monotone

modified theorem Ordinal.principal_iff_principal_swap

modified theorem Ordinal.principal_mul_iff_le_two_or_omega0_opow_opow

modified theorem Ordinal.principal_mul_iff_mul_left_eq

modified theorem Ordinal.principal_mul_of_le_two

modified theorem Ordinal.principal_swap_iff