Commit 2023-04-07 11:11 dc37f26f

View on Github →

chore: rename castLT (#3320) From #2450:

castSucc_cast_lt is misnamed, it should be castSucc_castLt. I wonder why mathport can't align it. This PR goes one step further and renames castLt to castLT everywhere, per https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/!4.233320/near/347567570.

Estimated changes

added theorem Fin.castAdd_castLT
deleted theorem Fin.castAdd_castLt
added def Fin.castLT
added theorem Fin.castLT_castAdd
added theorem Fin.castLT_castSucc
added theorem Fin.castLT_mk
added theorem Fin.castLT_succAbove
deleted def Fin.castLt
deleted theorem Fin.castLt_castAdd
deleted theorem Fin.castLt_mk
deleted theorem Fin.castLt_succAbove
added theorem Fin.castSucc_castLT
deleted theorem Fin.castSucc_cast_lt
deleted theorem Fin.cast_lt_castSucc
added theorem Fin.coe_castLT
deleted theorem Fin.coe_castLt
added theorem Fin.succAbove_castLT
deleted theorem Fin.succAbove_castLt