Def FinVec.mkSumEqQ

Modification history

2025-11-19 06:07

Mathlib/Data/Fin/Tuple/Reflection.lean

chore: move Mathlib to the module system (#31786) …

Deleted FinVec.mkSumEqQ View on Github →

2025-04-26 23:10

Mathlib/Data/Fin/Tuple/Reflection.lean

feat(Algebra/BigOperators): simprocify `prod_univ_one/two/three/...` (#23425) …

Added FinVec.mkSumEqQ View on Github →