List repetition utilities

Defines nTimes (notation l ^+^ n), the n-fold repetition of a list, together with basic rewriting lemmas about it.

def nTimes {α : Type u_1} (l : List α) (n : ℕ) : List α

nTimes l n (notation l ^+^ n) is the concatenation of n copies of the list l.

Equations

• l ^+^ n = (List.replicate n l).flatten

def «term_^+^_» : Lean.TrailingParserDescr

nTimes l n (notation l ^+^ n) is the concatenation of n copies of the list l.

Equations

• «term_^+^_» = Lean.ParserDescr.trailingNode `«term_^+^_» 69 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^+^ ") (Lean.ParserDescr.cat `term 70))

theorem nTimes_succ_l {α : Type u_1} {l : List α} {n : ℕ} : l ^+^ n.succ = l ++ l ^+^ n

theorem nTimes_succ_r {α : Type u_1} {l : List α} {n : ℕ} : l ^+^ n.succ = l ^+^ n ++ l

theorem nTimes_map {α : Type u_2} {l : List α} {n : ℕ} {β : Type u_1} {f : α → β} : List.map f l ^+^ n = List.map f (l ^+^ n)

theorem nTimes_add {α : Type u_1} {l : List α} {n m : ℕ} : l ^+^ (m + n) = l ^+^ m ++ l ^+^ n

theorem nTimes_mul {α : Type u_1} {l : List α} {n m : ℕ} : l ^+^ m * n = l ^+^ m ^+^ n