def Matrix.«term_:>_» : Lean.TrailingParserDescr

Equations

• Matrix.«term_:>_» = Lean.ParserDescr.trailingNode `Matrix.«term_:>_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :> ") (Lean.ParserDescr.cat `term 70))

@[simp]

theorem Matrix.vecCons_zero {α✝ : Type u_1} {a : α✝} {n✝ : ℕ} {s : Fin n✝ → α✝} : (a :> s) 0 = a

@[simp]

theorem Matrix.vecCons_succ {n : ℕ} {α✝ : Type u_1} {a : α✝} {s : Fin n → α✝} (i : Fin n) : (a :> s) i.succ = s i

@[simp]

theorem Matrix.vecCons_last {n : ℕ} {C : Type u_1} (a : C) (s : Fin (n + 1) → C) : (a :> s) (Fin.last (n + 1)) = s (Fin.last n)

def Matrix.vecConsLast {α : Type u} {n : ℕ} (t : Fin n → α) (h : α) : Fin n.succ → α

Equations

• (t <: h) i = Fin.lastCases h t i

@[simp]

theorem Matrix.cons_app_one {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ → α) : (a :> s) 1 = s 0

@[simp]

theorem Matrix.cons_app_two {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ → α) : (a :> s) 2 = s 1

@[simp]

theorem Matrix.cons_app_three {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ → α) : (a :> s) 3 = s 2

@[simp]

theorem Matrix.cons_app_four {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ → α) : (a :> s) 4 = s 3

@[simp]

theorem Matrix.cons_app_five {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ → α) : (a :> s) 5 = s 4

@[simp]

theorem Matrix.cons_app_six {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ → α) : (a :> s) 6 = s 5

@[simp]

theorem Matrix.cons_app_seven {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 7 = s 6

@[simp]

theorem Matrix.cons_app_eight {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 8 = s 7

def Matrix.unexpandVecEmpty : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def Matrix.unexpandVecCons : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def Matrix.«term_<:_» : Lean.TrailingParserDescr

Equations

• Matrix.«term_<:_» = Lean.ParserDescr.trailingNode `Matrix.«term_<:_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <: ") (Lean.ParserDescr.cat `term 71))

@[simp]

theorem Matrix.rightConcat_last {n : ℕ} {α✝ : Type u_1} {s : Fin n → α✝} {a : α✝} : (s <: a) (Fin.last n) = a

@[simp]

theorem Matrix.rightConcat_castSucc {n : ℕ} {α✝ : Type u_1} {s : Fin n → α✝} {a : α✝} (i : Fin n) : (s <: a) i.castSucc = s i

@[simp]

theorem Matrix.rightConcat_zero {n : ℕ} {α : Type u} (a : α) (s : Fin n.succ → α) : (s <: a) 0 = s 0

@[simp]

theorem Matrix.zero_succ_eq_id {n : ℕ} : 0 :> Fin.succ = id

@[simp]

theorem Matrix.zero_cons_succ_eq_self {n : ℕ} {α : Type u} (f : Fin (n + 1) → α) : (f 0 :> fun (x : Fin n) => f x.succ) = f

theorem Matrix.eq_vecCons {n : ℕ} {C : Type u_1} (s : Fin (n + 1) → C) : s 0 :> s ∘ Fin.succ = s

theorem Matrix.eq_vecCons' {n : ℕ} {C : Type u_1} (s : Fin (n + 1) → C) : (s 0 :> fun (x : Fin n) => s x.succ) = s

@[simp]

theorem Matrix.vecCons_ext {n : ℕ} {α : Type u} (a₁ a₂ : α) (s₁ s₂ : Fin n → α) : a₁ :> s₁ = a₂ :> s₂ ↔ a₁ = a₂ ∧ s₁ = s₂

theorem Matrix.vecCons_assoc {n : ℕ} {α : Type u} (a b : α) (s : Fin n → α) : a :> s <: b = (a :> s) <: b

def Matrix.decVec {α : Type u_1} {n : ℕ} (v w : Fin n → α) : ((i : Fin n) → Decidable (v i = w i)) → Decidable (v = w)

Equations

• Matrix.decVec x_4 x_5 x_6 = ⋯.mpr (isTrue trivial)
• Matrix.decVec v w d = ⋯.mpr (⋯.mpr (⋯.mpr instDecidableAnd))

theorem Matrix.comp_vecCons {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (a : α) (s : Fin n → α) : (fun (x : Fin n.succ) => f ((a :> s) x)) = f a :> f ∘ s

theorem Matrix.comp_vecCons' {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (a : α) (s : Fin n → α) : (fun (x : Fin n.succ) => f ((a :> s) x)) = f a :> fun (i : Fin n) => f (s i)

theorem Matrix.comp_vecCons'' {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (a : α) (s : Fin n → α) : f ∘ (a :> s) = f a :> f ∘ s

theorem Matrix.comp_vecCons₂' {n : ℕ} {α : Type u} {β : Sort u_1} {γ : Type u_2} (g : β → γ) (f : α → β) (a : α) (s : Fin n → α) : (fun (x : Fin n.succ) => g (f ((a :> s) x))) = g (f a) :> fun (i : Fin n) => g (f (s i))

@[simp]

theorem Matrix.comp₀ {α : Type u} {δ✝ : Type u_1} {f : α → δ✝} : f ∘ ![] = ![]

@[simp]

theorem Matrix.comp₁ {α : Type u} {δ✝ : Type u_1} {f : α → δ✝} (a : α) : f ∘ ![a] = ![f a]

@[simp]

theorem Matrix.comp₂ {α : Type u} {δ✝ : Type u_1} {f : α → δ✝} (a₁ a₂ : α) : f ∘ ![a₁, a₂] = ![f a₁, f a₂]

@[simp]

theorem Matrix.comp₃ {α : Type u} {δ✝ : Type u_1} {f : α → δ✝} (a₁ a₂ a₃ : α) : f ∘ ![a₁, a₂, a₃] = ![f a₁, f a₂, f a₃]

@[simp]

theorem Matrix.comp₄ {α : Type u} {δ✝ : Type u_1} {f : α → δ✝} (a₁ a₂ a₃ a₄ : α) : f ∘ ![a₁, a₂, a₃, a₄] = ![f a₁, f a₂, f a₃, f a₄]

theorem Matrix.comp_vecConsLast {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (a : α) (s : Fin n → α) : (fun (x : Fin n.succ) => f ((s <: a) x)) = f ∘ s <: f a

@[simp]

theorem Matrix.vecHead_comp {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (v : Fin (n + 1) → α) : vecHead (f ∘ v) = f (vecHead v)

@[simp]

theorem Matrix.vecTail_comp {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (v : Fin (n + 1) → α) : vecTail (f ∘ v) = f ∘ vecTail v

theorem Matrix.vecConsLast_vecEmpty {α : Type u} {s : Fin 0 → α} (a : α) : s <: a = ![a]

theorem Matrix.constant_eq_singleton {α : Type u} {a : α} : (fun (x : Fin (Nat.succ 0)) => a) = ![a]

theorem Matrix.fun_eq_vec_one {α : Type u} (v : Fin 1 → α) : v = ![v 0]

theorem Matrix.constant_eq_vec₂ {α : Type u} {a : α} : (fun (x : Fin (Nat.succ 0).succ) => a) = ![a, a]

theorem Matrix.fun_eq_vec_two {α : Type u} (v : Fin 2 → α) : v = ![v 0, v 1]

theorem Matrix.fun_eq_vec_three {α : Type u} (v : Fin 3 → α) : v = ![v 0, v 1, v 2]

theorem Matrix.fun_eq_vec_four {α : Type u} (v : Fin 4 → α) : v = ![v 0, v 1, v 2, v 3]

theorem Matrix.fun_eq_vec_four' {α : Type u} {β : Type u_1} (f : α → β) (v : Fin 4 → α) : f ∘ v = ![f (v 0), f (v 1), f (v 2), f (v 3)]

theorem Matrix.injective_vecCons {n : ℕ} {α : Type u} {f : Fin n → α} (h : Function.Injective f) {a : α} (ha : ∀ (i : Fin n), a ≠ f i) : Function.Injective (a :> f)

@[simp]

theorem Matrix.vecCons_empty_eq_singleton {α : Type u} (v : Fin 0 → α) (x : α) : x :> v = ![x]

@[simp]

theorem Matrix.vecConsLast_empty_eq_singleton {α : Type u} (v : Fin 0 → α) (x : α) : v <: x = ![x]

def Matrix.toList {α : Type u_1} {n : ℕ} : (Fin n → α) → List α

Equations

• Matrix.toList x_2 = []
• Matrix.toList v = v 0 :: Matrix.toList (v ∘ Fin.succ)

@[simp]

theorem Matrix.toList_zero {α : Type u_1} (v : Fin 0 → α) : toList v = []

@[simp]

theorem Matrix.toList_succ {α : Type u_1} {n : ℕ} (v : Fin (n + 1) → α) : toList v = v 0 :: toList (v ∘ Fin.succ)

@[simp]

theorem Matrix.toList_length {α : Type u_1} {n : ℕ} (v : Fin n → α) : (toList v).length = n

@[simp]

theorem Matrix.mem_toList_iff {α : Type u_1} {n : ℕ} {v : Fin n → α} {a : α} : a ∈ toList v ↔ ∃ (i : Fin n), v i = a

def Matrix.getM {m : Type u → Type v} [Monad m] {n : ℕ} {β : Fin n → Type u} : ((i : Fin n) → m (β i)) → m ((i : Fin n) → β i)

Equations

• Matrix.getM x_4 = pure finZeroElim
• Matrix.getM f = (fun (zero : x_3 0) (succ : (i : Fin n) → x_3 i.succ) (i : Fin (n + 1)) => Fin.cases zero succ i) <$> f 0 <*> Matrix.getM fun (x : Fin n) => f x.succ

theorem Matrix.getM_pure {m : Type u → Type v} [Monad m] [LawfulMonad m] {n : ℕ} {β : Fin n → Type u} (v : (i : Fin n) → β i) : (getM fun (i : Fin n) => pure (v i)) = pure v

@[simp]

theorem Matrix.getM_some {n : ℕ} {β : Fin n → Type u} (v : (i : Fin n) → β i) : (getM fun (i : Fin n) => some (v i)) = some v

def Matrix.appendr {α : Type w} {n m : ℕ} (v : Fin n → α) (w : Fin m → α) : Fin (m + n) → α

Equations

• Matrix.appendr v w = Matrix.vecAppend ⋯ v w

@[simp]

theorem Matrix.appendr_nil {α : Type w} {m : ℕ} (w : Fin m → α) : appendr ![] w = w

@[simp]

theorem Matrix.appendr_cons {α : Type w} {m n : ℕ} (x : α) (v : Fin n → α) (w : Fin m → α) : appendr (x :> v) w = x :> appendr v w

theorem Matrix.vecForall_iff {α : Type w} {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) : (∀ (v : Fin (n + 1) → α), φ v) ↔ ∀ (a : α) (v : Fin n → α), φ (a :> v)

theorem Matrix.vecExists_iff {α : Type w} {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) : (∃ (v : Fin (n + 1) → α), φ v) ↔ ∃ (a : α) (v : Fin n → α), φ (a :> v)

def Matrix.foldr {α : Type w} {β : Type u} (f : α → β → β) (init : β) {k : ℕ} : (Fin k → α) → β

Equations

• Matrix.foldr f init x_2 = init
• Matrix.foldr f init v = f (Matrix.vecHead v) (Matrix.foldr f init (Matrix.vecTail v))

def Matrix.vecMap {α : Type w} {β : Type u} {k : ℕ} (f : α → β) : (Fin k → α) → Fin k → β

Equations

• f⨟ v = f ∘ v

def Matrix.«term_⨟» : Lean.TrailingParserDescr

Equations

• Matrix.«term_⨟» = Lean.ParserDescr.trailingNode `Matrix.«term_⨟» 1024 1024 (Lean.ParserDescr.symbol "⨟")

@[simp]

theorem Matrix.vecMap_nil {α : Type w} {β : Type u} (f : α → β) (v : Fin 0 → α) : f⨟ v = ![]

@[simp]

theorem Matrix.vecMap_cons {α : Type w} {β : Type u} (f : α → β) {k : ℕ} (a : α) (v : Fin k → α) : f⨟ (a :> v) = f a :> f⨟ v

@[simp]

theorem Matrix.vecMap_cons' {α : Type w} {β : Type u} (f : α → β) {k : ℕ} (v : Fin (k + 1) → α) : f⨟ v = f (vecHead v) :> f⨟ (vecTail v)

@[simp]

theorem Matrix.vecMap_app {α : Type w} {β : Type u} (f : α → β) {k : ℕ} (v : Fin k → α) (i : Fin k) : f⨟ v i = f (v i)

theorem Matrix.vecMap_vecMap_comp {α : Type w} {β : Type u} {γ : Type u_1} {k : ℕ} (g : β → γ) (f : α → β) (v : Fin k → α) : g⨟ (f⨟ v) = (g ∘ f)⨟ v

theorem Matrix.vecMap_vecMap_comp' {α : Type w} {β : Type u} {γ : Type u_1} {k : ℕ} (g : β → γ) (f : α → β) (v : Fin k → α) : g⨟ (f⨟ v) = (fun (x : α) => g (f x))⨟ v

@[simp]

theorem Matrix.foldr_zero {α : Type w} {β : Type u} (f : α → β → β) (init : β) (v : Fin 0 → α) : foldr f init v = init

@[simp]

theorem Matrix.foldr_succ {α : Type w} {β : Type u} (f : α → β → β) (init : β) {k : ℕ} (v : Fin (k + 1) → α) : foldr f init v = f (vecHead v) (foldr f init (vecTail v))

def Matrix.foldl {α : Type w} {β : Type u} (f : α → β → α) (init : α) {k : ℕ} : (Fin k → β) → α

Equations

• Matrix.foldl f x✝ x_3 = x✝
• Matrix.foldl f x✝ v = Matrix.foldl f (f x✝ (Matrix.vecHead v)) (Matrix.vecTail v)

@[simp]

theorem Matrix.foldl_zero {α : Type w} {β : Type u} (f : α → β → α) (init : α) (v : Fin 0 → β) : foldl f init v = init

@[simp]

theorem Matrix.foldl_succ {α : Type w} {β : Type u} (f : α → β → α) (init : α) {k : ℕ} (v : Fin (k + 1) → β) : foldl f init v = foldl f (f init (vecHead v)) (vecTail v)

theorem Matrix.eq_iff_eq_vecHead_of_eq_vecTail {α : Type w} {n : ℕ} {v₁ v₂ : Fin (n + 1) → α} : vecHead v₁ = vecHead v₂ ∧ vecTail v₁ = vecTail v₂ ↔ v₁ = v₂

def Matrix.vecToNat {n : ℕ} (v : Fin n → ℕ) : ℕ

Equations

• Matrix.vecToNat v = Matrix.foldr (fun (x ih : ℕ) => Nat.pair x ih + 1) 0 v

@[simp]

theorem Matrix.vecToNat_empty (v : Fin 0 → ℕ) : vecToNat v = 0

@[simp]

theorem Matrix.encode_succ {n : ℕ} (x : ℕ) (v : Fin n → ℕ) : vecToNat (x :> v) = Nat.pair x (vecToNat v) + 1

@[simp]

theorem Matrix.appeendr_addCast {α : Type w} {m n : ℕ} (u : Fin m → α) (v : Fin n → α) (i : Fin m) : appendr u v (Fin.addCast n i) = u i

@[simp]

theorem Matrix.appeendr_addNat {α : Type w} {m n : ℕ} (u : Fin m → α) (v : Fin n → α) (i : Fin n) : appendr u v (i.addNat m) = v i