mathlib3

f694c7de - refactor(*): define `list.replicate` and migrate to it (#18127)

refactor(*): define `list.replicate` and migrate to it (#18127) This definition differs from `list.repeat` by the order of arguments. The new order is in sync with the Lean 4 version.