Commit 2023-01-19 10:05 438cdc86
View on Github →feat: introduce a new Fin.append and Fin.repeat (#1637) Port of https://github.com/leanprover-community/mathlib/pull/10346
feat: introduce a new Fin.append and Fin.repeat (#1637) Port of https://github.com/leanprover-community/mathlib/pull/10346