Commit 2024-08-19 07:42 98b8c758

View on Github →

chore(SetTheory/Ordinal/Principal): clean up formatting (#15953) This PR does the following:

Clean up some term mode sorcery.
Use the ω notation throughout.
Remove unneeded parentheses.
Indent proofs correctly.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Principal.lean

modified theorem Ordinal.Principal.iterate_lt

modified theorem Ordinal.add_absorp

modified theorem Ordinal.add_omega

modified theorem Ordinal.add_omega_opow

modified theorem Ordinal.mul_lt_omega_opow

modified theorem Ordinal.mul_omega

modified theorem Ordinal.mul_omega_dvd

modified theorem Ordinal.mul_omega_opow_opow

modified theorem Ordinal.nfp_le_of_principal

added theorem Ordinal.not_principal_iff

modified theorem Ordinal.op_eq_self_of_principal

modified theorem Ordinal.opow_omega

modified theorem Ordinal.principal_add_omega

modified theorem Ordinal.principal_add_omega_opow

modified theorem Ordinal.principal_iff_principal_swap

modified theorem Ordinal.principal_mul_omega

modified theorem Ordinal.principal_mul_omega_opow_opow

modified theorem Ordinal.principal_mul_two

modified theorem Ordinal.principal_one_iff

modified theorem Ordinal.principal_opow_omega

added theorem Ordinal.principal_swap_iff

modified theorem Ordinal.principal_zero