Commit 2023-06-09 00:56 8dbcc1dc

View on Github →

chore: fix lift_fun -> liftFun in lemma names (#4873)

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.liftFun_iff_succ

deleted theorem Fin.lift_fun_iff_succ

Modified Mathlib/Data/Fin/Tuple/Monotone.lean

added theorem liftFun_vecCons

deleted theorem lift_fun_vecCons

Modified Mathlib/Order/Antisymmetrization.lean