def Hex.Matrix.diagMatrix {R : Type u} [Zero R] {r : Nat} (d : Vector R r) (n m : Nat) : Matrix R n m

The n × m matrix carrying d down its leading diagonal. Entries past the length of d, and all off-diagonal entries, are zero.

Equations

• Hex.Matrix.diagMatrix d n m = Hex.Matrix.ofFn fun (i : Fin n) (j : Fin m) => if h : ↑i = ↑j ∧ ↑i < r then d[⟨↑i, ⋯⟩] else 0

theorem Hex.Matrix.getElem_diagMatrix {R : Type u} [Zero R] {r n m : Nat} (d : Vector R r) (i : Fin n) (j : Fin m) : (diagMatrix d n m)[i][j] = if h : ↑i = ↑j ∧ ↑i < r then d[⟨↑i, ⋯⟩] else 0

Entry formula for diagMatrix.

@[simp]

theorem Hex.Matrix.getElem_diagMatrix_of_eq {R : Type u} [Zero R] {r n m : Nat} (d : Vector R r) (i : Fin n) (j : Fin m) (hij : ↑i = ↑j) (hir : ↑i < r) : (diagMatrix d n m)[i][j] = d[⟨↑i, hir⟩]

An entry of diagMatrix on its represented diagonal is the corresponding vector entry.

@[simp]

theorem Hex.Matrix.getElem_diagMatrix_of_ne {R : Type u} [Zero R] {r n m : Nat} (d : Vector R r) (i : Fin n) (j : Fin m) (hij : ↑i ≠ ↑j) : (diagMatrix d n m)[i][j] = 0

An off-diagonal entry of diagMatrix is zero.

@[simp]

theorem Hex.Matrix.getElem_diagMatrix_of_ge {R : Type u} [Zero R] {r n m : Nat} (d : Vector R r) (i : Fin n) (j : Fin m) (hir : r ≤ ↑i) : (diagMatrix d n m)[i][j] = 0

A diagonal entry past the represented vector is zero.

@[simp]

theorem Hex.Matrix.diagMatrix_apply_of_ne {R : Type u} [Zero R] {r n m : Nat} (d : Vector R r) (i : Fin n) (j : Fin m) (hij : ↑i ≠ ↑j) : (diagMatrix d n m)[i][j] = 0

Compatibility name for an off-diagonal entry of diagMatrix.

@[simp]

theorem Hex.Matrix.diagMatrix_apply_diag {R : Type u} [Zero R] {r n m : Nat} (d : Vector R r) (i : Fin n) (j : Fin m) (hij : ↑i = ↑j) (hir : ↑i < r) : (diagMatrix d n m)[i][j] = d[⟨↑i, hir⟩]

Compatibility name for a represented diagonal entry of diagMatrix.

@[simp]

theorem Hex.Matrix.diagMatrix_apply_of_ge {R : Type u} [Zero R] {r n m : Nat} (d : Vector R r) (i : Fin n) (j : Fin m) (hir : r ≤ ↑i) : (diagMatrix d n m)[i][j] = 0

Compatibility name for a diagonal entry past the represented vector.

@[simp]

theorem Hex.Matrix.row_diagMatrix_of_ge {R : Type u} [Zero R] {r n m : Nat} (d : Vector R r) (i : Fin n) (hir : r ≤ ↑i) : (diagMatrix d n m).row i = 0

A row beyond the represented diagonal is zero.

theorem Hex.Matrix.row_diagMatrix_cast {R : Type u} [Lean.Grind.Semiring R] {r n m : Nat} (d : Vector R r) (hrn : r ≤ n) (hrm : r ≤ m) (i : Fin r) : (diagMatrix d n m).row (Fin.castLE hrn i) = d[i] • Vector.unit R (Fin.castLE hrm i)

A represented row of a diagonal matrix is the corresponding scalar multiple of an ambient unit vector.