Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-04 18:18 8ff139a0

View on Github →

feat(data/equiv/fin): fin_sum_fin_equiv simp lemmas (#9001)

Estimated changes

Modified src/data/equiv/fin.lean

modified theorem fin_sum_fin_equiv_apply_left

modified theorem fin_sum_fin_equiv_apply_right

added theorem fin_sum_fin_equiv_symm_apply_cast_add

added theorem fin_sum_fin_equiv_symm_apply_cast_add_right