Def Array.flatten

Modification history

2022-09-04 16:26

Mathlib/Data/Array/Defs.lean

feat: depend on std4 (#397)

Deleted Array.flatten View on Github →

2022-03-22 05:33

Mathlib/Data/Array/Defs.lean

feat: extended `have` and `let` tactics (#232)

Added Array.flatten View on Github →