@[simp]

theorem Fin.mul_add_div {m n : ℕ} (i : Fin m) (j : Fin n) : (↑i * n + ↑j) / n = ↑i

@[simp]

theorem Fin.mul_add_mod {n : ℕ} (j : Fin n) : ↑j % n = ↑j

@[simp]

theorem Fin.mul_add_lt_mul {m n : ℕ} (i : Fin m) (j : Fin n) : ↑i * n + ↑j < m * n

@[simp]

theorem Fin.mul_add_divNat {m n : ℕ} (i : Fin m) (j : Fin n) : ⟨↑i * n + ↑j, ⋯⟩.divNat = i

@[simp]

theorem Fin.mul_add_modNat {m n : ℕ} (i : Fin m) (j : Fin n) : ⟨↑i * n + ↑j, ⋯⟩.modNat = j

structure NMatrix (m n : ℕ) (α : Type u_1) : Type u_1

• data : Vector α (m * n)

def MatrixNotation.«termN𝕄[_,_,_]» : Lean.ParserDescr

Equations

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

@[inline]

def NMatrix.get {m n : ℕ} {α : Type u_1} (M : NMatrix m n α) (i : Fin m) (j : Fin n) : α

Equations

• M.get i j = M.data[↑i * n + ↑j]

theorem NMatrix.ext_get {m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} (h : ∀ (i : Fin m) (j : Fin n), X.get i j = X'.get i j) : X = X'

theorem NMatrix.ext_get_iff {m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} : (∀ (i : Fin m) (j : Fin n), X.get i j = X'.get i j) ↔ X = X'

@[inline, specialize #[]]

def NMatrix.ofFn {m n : ℕ} {α : Type u_1} : Matrix (Fin m) (Fin n) α ≃ NMatrix m n α

Equations

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

theorem NMatrix.get_inj {m n : ℕ} {α : Type u_1} : Function.Injective get

@[implicit_reducible]

instance NMatrix.instFunLikeFinForall {m n : ℕ} {α : Type u_1} : FunLike (NMatrix m n α) (Fin m) (Fin n → α)

Equations

• NMatrix.instFunLikeFinForall = { coe := NMatrix.get, coe_injective' := ⋯ }

@[simp]

theorem NMatrix.get_eq_apply {m n : ℕ} {α : Type u_1} {X : NMatrix m n α} {i : Fin m} : X.get i = X i

def NMatrix.set {m n : ℕ} {α : Type u_1} (M : NMatrix m n α) (i : Fin m) (j : Fin n) (a : α) : NMatrix m n α

Equations

• M.set i j a = { data := M.data.set (↑i * n + ↑j) a ⋯ }

theorem NMatrix.ext {m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} (h : ∀ (i : Fin m) (j : Fin n), X i j = X' i j) : X = X'

theorem NMatrix.ext_iff {m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} : X = X' ↔ ∀ (i : Fin m) (j : Fin n), X i j = X' i j

@[simp]

theorem NMatrix.mk_apply {m n : ℕ} {α : Type u_1} {data : Vector α (m * n)} {i : Fin m} {j : Fin n} : { data := data } i j = data[↑i * n + ↑j]

@[simp]

theorem NMatrix.data_getElem {m n : ℕ} {α : Type u_1} (M : NMatrix m n α) (i : Fin m) (j : Fin n) : M.data[↑i * n + ↑j] = M i j

theorem NMatrix.set_apply {m n : ℕ} {α : Type u_1} (M : NMatrix m n α) (i : Fin m) (j : Fin n) (a : α) (i' : Fin m) (j' : Fin n) : (M.set i j a) i' j' = if i = i' ∧ j = j' then a else M i' j'

@[simp]

theorem NMatrix.ofFn_apply {m n : ℕ} {α : Type u_1} {f : Fin m → Fin n → α} {i : Fin m} : (ofFn f) i = f i

@[simp]

theorem NMatrix.apply_ofFn {m n : ℕ} {α : Type u_1} {X : NMatrix m n α} : ofFn ⇑X = X

def NMatrix.ofMatrix {m n : ℕ} {α : Type u_1} : Matrix (Fin m) (Fin n) α ≃ NMatrix m n α

Alias of NMatrix.ofFn.

Equations

• @NMatrix.ofMatrix = @NMatrix.ofFn

@[reducible, inline]

abbrev NMatrix.asMatrix {m n : ℕ} {α : Type u_1} : NMatrix m n α ≃ Matrix (Fin m) (Fin n) α

Equations

• NMatrix.asMatrix = NMatrix.ofFn.symm

theorem NMatrix.asMatrix_eq_apply {m n : ℕ} {α : Type u_1} {X : NMatrix m n α} : asMatrix X = ⇑X

@[simp]

theorem NMatrix.asMatrix_apply {m n : ℕ} {α : Type u_1} {X : NMatrix m n α} {i : Fin m} : asMatrix X i = X i

@[simp]

theorem NMatrix.ofMatrix_apply {m n : ℕ} {α : Type u_1} {M : Matrix (Fin m) (Fin n) α} {i : Fin m} : (ofMatrix M) i = M i

@[simp]

theorem NMatrix.ofMatrix_apply₂ {m n : ℕ} {α : Type u_1} {M : Matrix (Fin m) (Fin n) α} {i : Fin m} {j : Fin n} : (ofMatrix M) i j = M i j

theorem NMatrix.eq_of_asMatrix {m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} (h : asMatrix X = asMatrix X') : X = X'

def NMatrix.fromBlocks {m m' n n' : ℕ} {α : Type u_1} (m₁₁ : NMatrix m n α) (m₁₂ : NMatrix m n' α) (m₂₁ : NMatrix m' n α) (m₂₂ : NMatrix m' n' α) : NMatrix (m + m') (n + n') α

Equations

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

def NMatrix.«termNB[[_,_],[_,_]]» : Lean.ParserDescr

Equations

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

def NMatrix.toBlocks₁₁ {m m' n n' : ℕ} {α : Type u_1} (M : NMatrix (m + m') (n + n') α) : NMatrix m n α

Equations

• M.toBlocks₁₁ = NMatrix.ofFn fun (i : Fin m) (j : Fin n) => M ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

def NMatrix.toBlocks₁₂ {m m' n n' : ℕ} {α : Type u_1} (M : NMatrix (m + m') (n + n') α) : NMatrix m n' α

Equations

• M.toBlocks₁₂ = NMatrix.ofFn fun (i : Fin m) (j : Fin n') => M ⟨↑i, ⋯⟩ ⟨n + ↑j, ⋯⟩

def NMatrix.toBlocks₂₁ {m m' n n' : ℕ} {α : Type u_1} (M : NMatrix (m + m') (n + n') α) : NMatrix m' n α

Equations

• M.toBlocks₂₁ = NMatrix.ofFn fun (i : Fin m') (j : Fin n) => M ⟨m + ↑i, ⋯⟩ ⟨↑j, ⋯⟩

def NMatrix.toBlocks₂₂ {m m' n n' : ℕ} {α : Type u_1} (M : NMatrix (m + m') (n + n') α) : NMatrix m' n' α

Equations

• M.toBlocks₂₂ = NMatrix.ofFn fun (i : Fin m') (j : Fin n') => M ⟨m + ↑i, ⋯⟩ ⟨n + ↑j, ⋯⟩

@[simp]

theorem NMatrix.toBlocks₁₁_apply {m m' n n' : ℕ} {α : Type u_1} (M : NMatrix (m + m') (n + n') α) {i : Fin m} {j : Fin n} : M.toBlocks₁₁ i j = M ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

@[simp]

theorem NMatrix.toBlocks₁₂_apply {m m' n n' : ℕ} {α : Type u_1} (M : NMatrix (m + m') (n + n') α) {i : Fin m} {j : Fin n'} : M.toBlocks₁₂ i j = M ⟨↑i, ⋯⟩ ⟨n + ↑j, ⋯⟩

@[simp]

theorem NMatrix.toBlocks₂₁_apply {m m' n n' : ℕ} {α : Type u_1} (M : NMatrix (m + m') (n + n') α) {i : Fin m'} {j : Fin n} : M.toBlocks₂₁ i j = M ⟨m + ↑i, ⋯⟩ ⟨↑j, ⋯⟩

@[simp]

theorem NMatrix.toBlocks₂₂_apply {m m' n n' : ℕ} {α : Type u_1} (M : NMatrix (m + m') (n + n') α) {i : Fin m'} {j : Fin n'} : M.toBlocks₂₂ i j = M ⟨m + ↑i, ⋯⟩ ⟨n + ↑j, ⋯⟩

@[simp]

theorem NMatrix.fromBlocks_toBlocks₁₁ {m m' n n' : ℕ} {α : Type u_1} (m₁₁ : NMatrix m n α) (m₁₂ : NMatrix m n' α) (m₂₁ : NMatrix m' n α) (m₂₂ : NMatrix m' n' α) : NB[[m₁₁, m₁₂],[m₂₁, m₂₂]].toBlocks₁₁ = m₁₁

@[simp]

theorem NMatrix.fromBlocks_toBlocks₁₂ {m m' n n' : ℕ} {α : Type u_1} (m₁₁ : NMatrix m n α) (m₁₂ : NMatrix m n' α) (m₂₁ : NMatrix m' n α) (m₂₂ : NMatrix m' n' α) : NB[[m₁₁, m₁₂],[m₂₁, m₂₂]].toBlocks₁₂ = m₁₂

@[simp]

theorem NMatrix.fromBlocks_toBlocks₂₁ {m m' n n' : ℕ} {α : Type u_1} (m₁₁ : NMatrix m n α) (m₁₂ : NMatrix m n' α) (m₂₁ : NMatrix m' n α) (m₂₂ : NMatrix m' n' α) : NB[[m₁₁, m₁₂],[m₂₁, m₂₂]].toBlocks₂₁ = m₂₁

@[simp]

theorem NMatrix.fromBlocks_toBlocks₂₂ {m m' n n' : ℕ} {α : Type u_1} (m₁₁ : NMatrix m n α) (m₁₂ : NMatrix m n' α) (m₂₁ : NMatrix m' n α) (m₂₂ : NMatrix m' n' α) : NB[[m₁₁, m₁₂],[m₂₁, m₂₂]].toBlocks₂₂ = m₂₂

@[simp]

theorem NMatrix.fromBlocks_get {m m' n n' : ℕ} {α : Type u_1} (m₁₁ : NMatrix m n α) (m₁₂ : NMatrix m n' α) (m₂₁ : NMatrix m' n α) (m₂₂ : NMatrix m' n' α) {i : Fin (m + m')} {j : Fin (n + n')} : NB[[m₁₁, m₁₂],[m₂₁, m₂₂]] i j = if hi : ↑i < m then if hj : ↑j < n then m₁₁ ⟨↑i, hi⟩ ⟨↑j, hj⟩ else m₁₂ ⟨↑i, hi⟩ ⟨↑j - n, ⋯⟩ else if hj : ↑j < n then m₂₁ ⟨↑i - m, ⋯⟩ ⟨↑j, hj⟩ else m₂₂ ⟨↑i - m, ⋯⟩ ⟨↑j - n, ⋯⟩

@[simp]

theorem NMatrix.toBlocks_fromBlocks {m m' n n' : ℕ} {α : Type u_1} (M : NMatrix (m + m') (n + n') α) : NB[[M.toBlocks₁₁, M.toBlocks₁₂],[M.toBlocks₂₁, M.toBlocks₂₂]] = M

def NMatrix.fill {m n : ℕ} {α : Type u_1} (a : α) : NMatrix m n α

Equations

• NMatrix.fill a = NMatrix.ofFn fun (x : Fin m) (x_1 : Fin n) => a

@[simp]

def NMatrix.fill_apply {m n : ℕ} {α : Type u_1} {a : α} {i : Fin m} {j : Fin n} : (fill a) i j = a

Equations

• ⋯ = ⋯

@[simp]

theorem NMatrix.asMatrix_ofMatrix {m n : ℕ} {α : Type u_1} {X : NMatrix m n α} : ofMatrix (asMatrix X) = X

@[simp]

theorem NMatrix.ofMatrix_asMatrix {m n : ℕ} {α : Type u_1} {M : Matrix (Fin m) (Fin n) α} : asMatrix (ofMatrix M) = M

@[simp]

theorem NMatrix.ofFn_asMatrix {m n : ℕ} {α : Type u_1} {f : Fin m → Fin n → α} : asMatrix (ofFn f) = f

def NMatrix.map {m n : ℕ} {α : Type u_1} {β : Type u_2} (M : NMatrix m n α) (f : α → β) : NMatrix m n β

Equations

• M.map f = { data := Vector.map f M.data }

@[simp]

theorem NMatrix.map_apply {m n : ℕ} {α : Type u_1} {β : Type u_2} (M : NMatrix m n α) (f : α → β) {i : Fin m} {j : Fin n} : (M.map f) i j = f (M i j)

@[implicit_reducible]

instance NMatrix.instOneOfZero {n : ℕ} {α : Type u_1} [Zero α] [One α] : One (NMatrix n n α)

Equations

• NMatrix.instOneOfZero = { one := NMatrix.ofFn fun (i j : Fin n) => if i = j then 1 else 0 }

@[implicit_reducible]

instance NMatrix.instZero {m n : ℕ} {α : Type u_1} [Zero α] : Zero (NMatrix m n α)

Equations

• NMatrix.instZero = { zero := NMatrix.fill 0 }

@[simp]

theorem NMatrix.zero_apply {m n : ℕ} {α : Type u_1} [Zero α] {i : Fin m} {j : Fin n} : 0 i j = 0

@[simp]

theorem NMatrix.one_apply {n : ℕ} {α : Type u_1} [Zero α] [One α] {i j : Fin n} : 1 i j = if i = j then 1 else 0

def NMatrix.slowAdd {m n : ℕ} {α : Type u_1} [Add α] (a b : NMatrix m n α) : NMatrix m n α

Equations

• a.slowAdd b = NMatrix.ofMatrix (NMatrix.asMatrix a + NMatrix.asMatrix b)

@[specialize #[]]

def NMatrix.fastAdd {m n : ℕ} {α : Type u_1} [Add α] (X Y : NMatrix m n α) : NMatrix m n α

Equations

• X.fastAdd Y = { data := X.data + Y.data }

@[csimp]

theorem NMatrix.slowAdd_eq_fastAdd : @slowAdd = @fastAdd

@[implicit_reducible]

instance NMatrix.instAdd {m n : ℕ} {α : Type u_1} [Add α] : Add (NMatrix m n α)

Equations

• NMatrix.instAdd = { add := NMatrix.slowAdd }

def NMatrix.slowMul {l m n : ℕ} {α : Type u_1} [Mul α] [AddCommMonoid α] (a : NMatrix l m α) (b : NMatrix m n α) : NMatrix l n α

Equations

• a.slowMul b = NMatrix.ofMatrix (NMatrix.asMatrix a * NMatrix.asMatrix b)

@[specialize #[]]

def NMatrix.fastMul' {l m n : ℕ} {α : Type u_1} [Mul α] [AddCommMonoid α] (X : NMatrix l m α) (Y : NMatrix m n α) : NMatrix l n α

Equations

• X.fastMul' Y = NMatrix.ofFn fun (r : Fin l) (c : Fin n) => Fin.sum fun (k : Fin m) => X r k * Y k c

@[implicit_reducible, defaultInstance 100]

instance NMatrix.instHMulOfMulOfAddCommMonoid {l m n : ℕ} {α : Type u_1} [Mul α] [AddCommMonoid α] : HMul (NMatrix l m α) (NMatrix m n α) (NMatrix l n α)

Equations

• NMatrix.instHMulOfMulOfAddCommMonoid = { hMul := NMatrix.slowMul }

@[implicit_reducible]

instance NMatrix.instMulOfAddCommMonoid {n : ℕ} {α : Type u_1} [Mul α] [AddCommMonoid α] : Mul (NMatrix n n α)

Equations

• NMatrix.instMulOfAddCommMonoid = { mul := fun (a b : NMatrix n n α) => a * b }

theorem NMatrix.add_def {m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} [Add α] : X + X' = ofMatrix (asMatrix X + asMatrix X')

theorem NMatrix.mul_def {l m n : ℕ} {α : Type u_1} {X : NMatrix m n α} {Y : NMatrix n l α} [Mul α] [AddCommMonoid α] : X * Y = ofMatrix (asMatrix X * asMatrix Y)

@[simp]

theorem NMatrix.add_apply {m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} [Add α] {i : Fin m} : (X + X') i = X i + X' i

@[implicit_reducible]

instance NMatrix.instAddCommMonoid {m n : ℕ} {α : Type u_1} [AddCommMonoid α] : AddCommMonoid (NMatrix m n α)

Equations

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

@[simp]

theorem NMatrix.sum_apply {m n : ℕ} {𝒮 : Type u_2} [AddCommMonoid 𝒮] {ι : Type u_3} {S : Finset ι} (f : ι → NMatrix m n 𝒮) {x : Fin m} {y : Fin n} : (∑ i ∈ S, f i) x y = ∑ i ∈ S, (f i) x y

@[csimp]

theorem NMatrix.slowMul_eq_fastMul : @slowMul = @fastMul'

@[simp]

theorem NMatrix.asMatrix_add {m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} [Add α] : asMatrix (X + X') = asMatrix X + asMatrix X'

@[simp]

theorem NMatrix.mul_coe {l m n : ℕ} {α : Type u_1} {X : NMatrix m n α} {Y : NMatrix n l α} [Mul α] [AddCommMonoid α] : ⇑(X * Y) = asMatrix X * asMatrix Y

theorem NMatrix.asMatrix_mul {l m n : ℕ} {α : Type u_1} {X : NMatrix m n α} {Y : NMatrix n l α} [Mul α] [AddCommMonoid α] : asMatrix (X * Y) = asMatrix X * asMatrix Y

theorem NMatrix.mul_assoc {l k m n : ℕ} {α : Type u_1} {X : NMatrix m n α} {Y : NMatrix n l α} {Z : NMatrix l k α} [NonUnitalSemiring α] : X * Y * Z = X * (Y * Z)

theorem NMatrix.add_assoc {m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} [AddSemigroup α] {X'' : NMatrix m n α} : X + X' + X'' = X + (X' + X'')

theorem NMatrix.add_comm {m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} [AddCommMonoid α] : X + X' = X' + X

theorem NMatrix.add_mul {l m n : ℕ} {α : Type u_1} {X X' : NMatrix m n α} {Y : NMatrix n l α} [Semiring α] : (X + X') * Y = X * Y + X' * Y

theorem NMatrix.mul_add {l m n : ℕ} {α : Type u_1} {X : NMatrix m n α} {Y Y' : NMatrix n l α} [Semiring α] : X * (Y + Y') = X * Y + X * Y'

@[simp]

theorem NMatrix.one_mul {m n : ℕ} {α : Type u_1} {X : NMatrix m n α} [Semiring α] : 1 * X = X

@[simp]

theorem NMatrix.mul_one {m n : ℕ} {α : Type u_1} {X : NMatrix m n α} [Semiring α] : X * 1 = X

@[simp]

theorem NMatrix.zero_mul {l m n : ℕ} {α : Type u_1} {X : NMatrix m n α} [NonUnitalSemiring α] : 0 * X = 0

@[simp]

theorem NMatrix.mul_zero {l m n : ℕ} {α : Type u_1} {X : NMatrix m n α} [NonUnitalSemiring α] : X * 0 = 0

@[simp]

theorem NMatrix.zero_add {m n : ℕ} {α : Type u_1} {X : NMatrix m n α} [NonUnitalSemiring α] : 0 + X = X

@[simp]

theorem NMatrix.add_zero {m n : ℕ} {α : Type u_1} {X : NMatrix m n α} [NonUnitalSemiring α] : X + 0 = X

@[implicit_reducible]

instance NMatrix.instSemiring {n : ℕ} {α : Type u_2} [Semiring α] : Semiring (NMatrix n n α)

Equations

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

@[implicit_reducible]

instance NMatrix.instPartialOrder {m n : ℕ} {α : Type u_2} [OmegaCompletePartialOrder α] : PartialOrder (NMatrix m n α)

Equations

• NMatrix.instPartialOrder = { le := fun (a b : NMatrix m n α) => NMatrix.asMatrix a ≤ NMatrix.asMatrix b, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[implicit_reducible]

instance NMatrix.instOmegaCompletePartialOrder {m n : ℕ} {α : Type u_2} [OmegaCompletePartialOrder α] : OmegaCompletePartialOrder (NMatrix m n α)

Equations

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

@[implicit_reducible]

instance NMatrix.instOrderBot {m n : ℕ} {α : Type u_2} [OmegaCompletePartialOrder α] [OrderBot α] : OrderBot (NMatrix m n α)

Equations

• NMatrix.instOrderBot = { bot := NMatrix.ofMatrix ⊥, bot_le := ⋯ }

instance NMatrix.instIsPositiveOrderedAddMonoid {m n : ℕ} {α : Type u_2} [OmegaCompletePartialOrder α] [OrderBot α] [AddCommMonoid α] [IsPositiveOrderedAddMonoid α] : IsPositiveOrderedAddMonoid (NMatrix m n α)

instance NMatrix.instMulLeftMono {n : ℕ} {α : Type u_2} [OmegaCompletePartialOrder α] [OrderBot α] [Semiring α] [IsPositiveOrderedAddMonoid α] [MulLeftMono α] : MulLeftMono (NMatrix n n α)

theorem NMatrix.fromBlocks_mul {α : Type u_1} {l m n o p q : ℕ} (A : NMatrix n l α) (B : NMatrix n m α) (C : NMatrix o l α) (D : NMatrix o m α) (A' : NMatrix l p α) (B' : NMatrix l q α) (C' : NMatrix m p α) (D' : NMatrix m q α) [NonUnitalSemiring α] : NB[[A, B],[C, D]] * NB[[A', B'],[C', D']] = NB[[A * A' + B * C', A * B' + B * D'],[C * A' + D * C', C * B' + D * D']]

theorem NMatrix.fromBlocks_add {α : Type u_1} {l m n o : ℕ} (A : NMatrix n l α) (B : NMatrix n m α) (C : NMatrix o l α) (D : NMatrix o m α) (A' : NMatrix n l α) (B' : NMatrix n m α) (C' : NMatrix o l α) (D' : NMatrix o m α) [Add α] : NB[[A, B],[C, D]] + NB[[A', B'],[C', D']] = NB[[A + A', B + B'],[C + C', D + D']]

theorem NMatrix.fromBlocks_eq_one {α : Type u_1} {m n : ℕ} [Semiring α] : NB[[1, 0],[0, 1]] = 1

@[simp]

theorem NMatrix.fromBlocks_le_iff {α : Type u_1} {l m n o : ℕ} (A : NMatrix n l α) (B : NMatrix n m α) (C : NMatrix o l α) (D : NMatrix o m α) (A' : NMatrix n l α) (B' : NMatrix n m α) (C' : NMatrix o l α) (D' : NMatrix o m α) [OmegaCompletePartialOrder α] : NB[[A, B],[C, D]] ≤ NB[[A', B'],[C', D']] ↔ A ≤ A' ∧ B ≤ B' ∧ C ≤ C' ∧ D ≤ D'

theorem NMatrix.fromBlocks_le {α : Type u_1} {l m n o : ℕ} (A : NMatrix n l α) (B : NMatrix n m α) (C : NMatrix o l α) (D : NMatrix o m α) (A' : NMatrix n l α) (B' : NMatrix n m α) (C' : NMatrix o l α) (D' : NMatrix o m α) [OmegaCompletePartialOrder α] (hA : A ≤ A') (hB : B ≤ B') (hC : C ≤ C') (hD : D ≤ D') : NB[[A, B],[C, D]] ≤ NB[[A', B'],[C', D']]

@[simp]

theorem NMatrix.ωSum_apply {m n : ℕ} {𝒮 : Type u_2} [AddCommMonoid 𝒮] {ι : Type u_3} [Countable ι] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (f : ι → NMatrix m n 𝒮) {x : Fin m} {y : Fin n} : (ω∑ (i : ι), f i) x y = ω∑ (i : ι), (f i) x y