Commit 2023-05-10 11:05 a614aa76

View on Github →

chore: forward-port leanprover-community/mathlib#18341 and leanprover-community/mathlib#18950 (#3807) This also brings the proof of partialProd_right_inv in line with mathlib3.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

added theorem Fin.inv_partialProd_mul_eq_contractNth

modified theorem Fin.partialProd_right_inv

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

added def Fin.contractNth

added theorem Fin.contractNth_apply_of_eq

added theorem Fin.contractNth_apply_of_gt

added theorem Fin.contractNth_apply_of_lt

added theorem Fin.contractNth_apply_of_ne