Commit 2022-08-29 13:10 1b8a0c29

View on Github →

chore(set_theory/cardinal/ordinal): follow your linter (#16265) Editing set_theory.cardinal.ordinal, I noticed that the linter was unhappy. So, I thought of pleasing it. I followed its instructions, but, admittedly, I do not know if this is a good change or not! I replaced some fintype assumptions by finite ones and changed one proof as a consequence.

Estimated changes

Modified src/set_theory/cardinal/ordinal.lean

modified theorem cardinal.extend_function_finite

modified theorem cardinal.mk_compl_eq_mk_compl_finite

modified theorem cardinal.mk_compl_eq_mk_compl_finite_lift

modified theorem cardinal.mk_compl_eq_mk_compl_finite_same