Commit 2025-01-28 16:01 3d93b8de

View on Github →

feat(/Fin/): add lemmas (#21175) Cherry-picked parts of #21112 that don't rely on a decision about inline haveI : NeZero n := _

Estimated changes

added theorem Fin.cast_inj
modified theorem Fin.bot_eq_zero
added theorem Fin.succ_top
added theorem Fin.top_eq_zero
added theorem Fin.val_top
added theorem Fin.zero_eq_top