def EMatrix (m : Type u_1) (n : Type u_2) (α : Type u_3) [Listed m] [Listed n] : Type u_3

Equations

• EMatrix m n α = NMatrix (Listed.size m) (Listed.size n) α

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

Equations

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

def EMatrix.getN {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] (M : EMatrix m n α) (i : Fin (Listed.size m)) (j : Fin (Listed.size n)) : α

Equations

• M.getN i j = NMatrix.get M i j

def EMatrix.get {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] (M : EMatrix m n α) (i : m) (j : n) : α

Equations

• M.get i j = M.getN (Listed.encodeFin i) (Listed.encodeFin j)

def EMatrix.asNMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] (X : EMatrix m n α) : NMatrix (Listed.size m) (Listed.size n) α

Equations

• X.asNMatrix = X

def EMatrix.asNMatrix₂ {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {m' : Type u_6} {n' : Type u_7} [Listed m'] [Listed n'] (X : EMatrix m n (EMatrix m' n' α)) : NMatrix (Listed.size m) (Listed.size n) (NMatrix (Listed.size m') (Listed.size n') α)

Equations

• X.asNMatrix₂ = X

theorem EMatrix.eq_of_asNMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X X' : EMatrix m n α} (h : X.asNMatrix = X'.asNMatrix) : X = X'

theorem EMatrix.ext_get {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X X' : EMatrix m n α} (h : ∀ (i : m) (j : n), X.get i j = X'.get i j) : X = X'

theorem EMatrix.get_inj {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] : Function.Injective get

@[implicit_reducible]

instance EMatrix.instFunLikeForall {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] : FunLike (EMatrix m n α) m (n → α)

Equations

• EMatrix.instFunLikeForall = { coe := EMatrix.get, coe_injective' := ⋯ }

@[simp]

theorem EMatrix.get_eq_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X : EMatrix m n α} {i : m} : X.get i = X i

@[simp]

theorem EMatrix.asNMatrix_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X : EMatrix m n α} {i : Fin (Listed.size m)} {j : Fin (Listed.size n)} : X.asNMatrix i j = X (Listed.decodeFin i) (Listed.decodeFin j)

@[simp]

theorem EMatrix.getN_eq {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X : EMatrix m n α} {i : Fin (Listed.size m)} {j : Fin (Listed.size n)} : X.getN i j = X (Listed.decodeFin i) (Listed.decodeFin j)

theorem EMatrix.ext {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X X' : EMatrix m n α} (h : ∀ (i : m) (j : n), X i j = X' i j) : X = X'

theorem EMatrix.ext_iff {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X X' : EMatrix m n α} : X = X' ↔ ∀ (i : m) (j : n), X i j = X' i j

def EMatrix.ofFn {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] : (Fin (Listed.size m) → Fin (Listed.size n) → α) → EMatrix m n α

Equations

• EMatrix.ofFn = ⇑NMatrix.ofFn

def EMatrix.ofFnSlow {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] (f : m → n → α) : EMatrix m n α

Equations

• EMatrix.ofFnSlow f = NMatrix.ofFn fun (i : Fin (Listed.size m)) (j : Fin (Listed.size n)) => f (Listed.decodeFin i) (Listed.decodeFin j)

def EMatrix.ofNMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] (N : NMatrix (Listed.size m) (Listed.size n) α) : EMatrix m n α

Equations

• EMatrix.ofNMatrix N = N

@[simp]

theorem EMatrix.ofFn_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {f : Fin (Listed.size m) → Fin (Listed.size n) → α} {i : m} {j : n} : (ofFn f) i j = f (Listed.encodeFin i) (Listed.encodeFin j)

@[simp]

theorem EMatrix.NMatrix_coe_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {M : EMatrix m n α} (i : m) (j : n) : M (Listed.encodeFin i) (Listed.encodeFin j) = M i j

@[simp]

theorem EMatrix.NMatrix_ofFn_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] (i : m) (j : n) {f : Matrix (Fin (Listed.size m)) (Fin (Listed.size n)) α} : (NMatrix.ofFn f) i j = f (Listed.encodeFin i) (Listed.encodeFin j)

@[simp]

theorem EMatrix.apply_ofFnSlow {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X : EMatrix m n α} : ofFnSlow ⇑X = X

@[simp]

theorem EMatrix.ofFnSlow_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {f : m → n → α} {i : m} : (ofFnSlow f) i = f i

def EMatrix.asMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] (M : EMatrix m n α) : Matrix m n α

Equations

• M.asMatrix = ⇑M

def EMatrix.ofMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] (M : Matrix m n α) : EMatrix m n α

Equations

• EMatrix.ofMatrix M = EMatrix.ofFnSlow M

@[simp]

theorem EMatrix.ofMatrix_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {f : m → n → α} {i : m} : (ofMatrix f) i = f i

@[simp]

theorem EMatrix.asMatrix_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {f : EMatrix m n α} {i : m} : f.asMatrix i = f i

@[simp]

theorem EMatrix.asMatrix_apply₂ {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {f : EMatrix m n α} {i : m} {j : n} : f.asMatrix i j = f i j

@[simp]

theorem EMatrix.asMatrix_ofMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X : EMatrix m n α} : ofMatrix X.asMatrix = X

@[simp]

theorem EMatrix.ofMatrix_asMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {M : Matrix m n α} : (ofMatrix M).asMatrix = M

def EMatrix.map {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {β : Type u_8} (f : α → β) (M : EMatrix m n α) : EMatrix m n β

Equations

• EMatrix.map f M = EMatrix.ofFn fun (i : Fin (Listed.size m)) (j : Fin (Listed.size n)) => f (M.getN i j)

def EMatrix.asMatrix₂ {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {m' : Type u_6} {n' : Type u_7} [Listed m'] [Listed n'] (M : EMatrix m n (EMatrix m' n' α)) : Matrix m n (Matrix m' n' α)

Equations

• M.asMatrix₂ i j i' j' = (M i j) i' j'

def EMatrix.ofMatrix₂ {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {m' : Type u_6} {n' : Type u_7} [Listed m'] [Listed n'] (M : Matrix m n (Matrix m' n' α)) : EMatrix m n (EMatrix m' n' α)

Equations

• EMatrix.ofMatrix₂ M = EMatrix.map EMatrix.ofMatrix (EMatrix.ofFnSlow M)

@[simp]

theorem EMatrix.asMatrix₂_ofMatrix₂ {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {m' : Type u_6} {n' : Type u_7} [Listed m'] [Listed n'] {X : EMatrix m n (EMatrix m' n' α)} : ofMatrix₂ X.asMatrix₂ = X

@[simp]

theorem EMatrix.ofMatrix₂_asMatrix₂ {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {m' : Type u_6} {n' : Type u_7} [Listed m'] [Listed n'] {M : Matrix m n (Matrix m' n' α)} : (ofMatrix₂ M).asMatrix₂ = M

theorem EMatrix.eq_ofMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X X' : EMatrix m n α} (h : X.asMatrix = X'.asMatrix) : X = X'

@[implicit_reducible]

instance EMatrix.instOneOfZero {n : Type u_3} {α : Type u_5} [Listed n] [Zero α] [One α] : One (EMatrix n n α)

Equations

• EMatrix.instOneOfZero = { one := EMatrix.instOneOfZero._aux_1 }

@[implicit_reducible]

instance EMatrix.instZero {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] [Zero α] : Zero (EMatrix m n α)

Equations

• EMatrix.instZero = { zero := EMatrix.instZero._aux_1 }

@[implicit_reducible]

instance EMatrix.instAdd {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] [Add α] : Add (EMatrix m n α)

Equations

• EMatrix.instAdd = { add := EMatrix.instAdd._aux_1 }

theorem EMatrix.add_def {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X X' : EMatrix m n α} [Add α] : X + X' = X.asNMatrix + X'.asNMatrix

theorem EMatrix.one_def {n : Type u_3} {α : Type u_5} [Listed n] [Zero α] [One α] : 1 = asNMatrix 1

theorem EMatrix.zero_def {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] [Zero α] : 0 = asNMatrix 0

theorem EMatrix.one_apply {n : Type u_3} {α : Type u_5} [Listed n] [DecidableEq n] [Zero α] [One α] {i j : n} : 1 i j = if i = j then 1 else 0

@[simp]

theorem EMatrix.zero_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] [Zero α] {i : m} {j : n} : 0 i j = 0

@[simp]

theorem EMatrix.zero_apply' {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] [Zero α] {i : m} {j : n} : (OfNat.ofNat 0) i j = 0

@[simp]

theorem EMatrix.zero_asMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] [Zero α] : asMatrix 0 = 0

@[implicit_reducible]

instance EMatrix.instHSMulOfMul {α : Type u_5} [Mul α] {X : Type u_8} {Y : Type u_9} [Listed X] [Listed Y] : HSMul α (EMatrix X Y α) (EMatrix X Y α)

Equations

• EMatrix.instHSMulOfMul = { hSMul := fun (s : α) (m : EMatrix X Y α) => EMatrix.map (fun (x : α) => s * x) m }

@[implicit_reducible]

instance EMatrix.instHSMulMulOppositeOfMul {α : Type u_5} [Mul α] {X : Type u_8} {Y : Type u_9} [Listed X] [Listed Y] : HSMul αᵐᵒᵖ (EMatrix X Y α) (EMatrix X Y α)

Equations

• EMatrix.instHSMulMulOppositeOfMul = { hSMul := fun (s : αᵐᵒᵖ) (m : EMatrix X Y α) => EMatrix.map (fun (x : α) => x * MulOpposite.unop s) m }

@[simp]

theorem EMatrix.NMatrix_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {M : Matrix (Fin (Listed.size m)) (Fin (Listed.size n)) α} {i : m} {j : n} : (NMatrix.ofMatrix M) i j = (NMatrix.ofMatrix M) (Listed.encodeFin i) (Listed.encodeFin j)

@[simp]

theorem EMatrix.add_apply {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X X' : EMatrix m n α} [Add α] {i : m} {j : n} : (X + X') i j = X i j + X' i j

@[simp]

theorem EMatrix.asMatrix_add {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] {X X' : EMatrix m n α} [Add α] : (X + X').asMatrix = X.asMatrix + X'.asMatrix

@[implicit_reducible, defaultInstance 100]

instance EMatrix.instHMul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed l] [Listed m] [Listed n] [Mul α] [AddCommMonoid α] : HMul (EMatrix l m α) (EMatrix m n α) (EMatrix l n α)

Equations

• EMatrix.instHMul = { hMul := EMatrix.instHMul._aux_1 }

@[implicit_reducible]

instance EMatrix.instMul {m : Type u_2} {α : Type u_5} [Listed m] [Mul α] [AddCommMonoid α] : Mul (EMatrix m m α)

Equations

• EMatrix.instMul = { mul := fun (a b : EMatrix m m α) => a * b }

@[simp]

theorem EMatrix.hmul_eq_hmul {m : Type u_2} {α : Type u_5} [Listed m] [Mul α] [AddCommMonoid α] : HMul.hMul = HMul.hMul

@[implicit_reducible]

instance EMatrix.instAddCommMonoid {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] [AddCommMonoid α] : AddCommMonoid (EMatrix m n α)

Equations

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

@[implicit_reducible, defaultInstance 100]

instance EMatrix.instSemiring {n : Type u_3} {α : Type u_5} [Listed n] [Semiring α] : Semiring (EMatrix n n α)

Equations

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

@[implicit_reducible]

instance EMatrix.instOmegaCompletePartialOrder {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] [OmegaCompletePartialOrder α] : OmegaCompletePartialOrder (EMatrix m n α)

Equations

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

@[implicit_reducible]

instance EMatrix.instOrderBot {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] [OmegaCompletePartialOrder α] [OrderBot α] : OrderBot (EMatrix m n α)

Equations

• EMatrix.instOrderBot = { bot := EMatrix.instOrderBot._aux_1, bot_le := ⋯ }

instance EMatrix.instIsPositiveOrderedAddMonoid {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed m] [Listed n] [AddCommMonoid α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] : IsPositiveOrderedAddMonoid (EMatrix m n α)

theorem EMatrix.mul_def {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed l] [Listed m] [Listed n] {X : EMatrix m n α} {Y : EMatrix n l α} [Mul α] [AddCommMonoid α] : X * Y = X.asNMatrix * Y.asNMatrix

theorem EMatrix.mul_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_5} [Listed l] [Listed m] [Listed n] {X : EMatrix m n α} {Y : EMatrix n l α} [Fintype n] [Mul α] [AddCommMonoid α] {a : m} {b : l} : (X * Y) a b = ∑ c : n, X a c * Y c b

theorem EMatrix.mul_assoc {l : Type u_1} {m : Type u_2} {n : Type u_3} {w : Type u_4} {α : Type u_5} [Listed l] [Listed m] [Listed n] [Listed w] {X : EMatrix m n α} {Y : EMatrix n l α} {Z : EMatrix l w α} [NonUnitalSemiring α] : X * Y * Z = X * (Y * Z)

@[simp]

theorem EMatrix.NMatrix.map_apply {m n : ℕ} {𝒮 : Type u_8} {𝒮' : Type u_9} {f : NMatrix m n 𝒮} {g : 𝒮 → 𝒮'} {i : Fin m} {j : Fin n} : (f.map g) i j = g (f i j)

@[simp]

theorem EMatrix.NMatrix.ofFn_map {m n : ℕ} {𝒮 : Type u_8} {𝒮' : Type u_9} {f : Fin m → Fin n → 𝒮} {g : 𝒮 → 𝒮'} : (NMatrix.ofFn f).map g = NMatrix.ofFn fun (i : Fin m) (j : Fin n) => g (f i j)

@[simp]

theorem EMatrix.ofFn_asMatrix {m : Type u_8} {n : Type u_9} {𝒮 : Type u_10} [Listed m] [Listed n] {f : Fin (Listed.size m) → Fin (Listed.size n) → 𝒮} : (ofFn f).asMatrix = fun (i : m) (j : n) => f (Listed.encodeFin i) (Listed.encodeFin j)

@[simp]

theorem EMatrix.map_apply {m : Type u_8} {n : Type u_9} {𝒮 : Type u_10} {𝒮' : Type u_11} [Listed m] [Listed n] {f : EMatrix m n 𝒮} {g : 𝒮 → 𝒮'} {i : m} {j : n} : (map g f) i j = g (f i j)

@[simp]

theorem EMatrix.map_asMatrix {m : Type u_8} {n : Type u_9} {𝒮 : Type u_10} {𝒮' : Type u_11} [Listed m] [Listed n] {f : EMatrix m n 𝒮} {g : 𝒮 → 𝒮'} {i : m} {j : n} : (map g f).asMatrix i j = g (f.asMatrix i j)

@[simp]

theorem EMatrix.ofMatrix₂_apply {m : Type u_8} {m' : Type u_9} {n : Type u_10} {n' : Type u_11} {𝒮 : Type u_12} [Listed m] [Listed n] [Listed m'] [Listed n'] {M : Matrix m n (Matrix m' n' 𝒮)} {i : m} {j : n} : (ofMatrix₂ M) i j = ofMatrix (M i j)

@[simp]

theorem EMatrix.toMatrix₂_ofMatrix₂ {m : Type u_8} {m' : Type u_9} {n : Type u_10} {n' : Type u_11} {𝒮 : Type u_12} [Listed m] [Listed n] [Listed m'] [Listed n'] {M : EMatrix m n (EMatrix m' n' 𝒮)} : ofMatrix₂ M.asMatrix₂ = M

@[simp]

theorem EMatrix.ofMatrix_add {m : Type u_8} {n : Type u_9} {𝒮 : Type u_10} [Listed m] [Listed n] [Add 𝒮] (a b : Matrix m n 𝒮) : ofMatrix (a + b) = ofMatrix a + ofMatrix b

@[simp]

theorem EMatrix.ofMatrix_sum {m : Type u_8} {n : Type u_9} {𝒮 : Type u_10} [Listed m] [Listed n] [AddCommMonoid 𝒮] {ι : Type u_11} {S : Finset ι} [DecidableEq ι] (f : ι → Matrix n m 𝒮) : ofMatrix (∑ i ∈ S, f i) = ∑ i ∈ S, ofMatrix (f i)

@[simp]

theorem EMatrix.ofMatrix_pow {m : Type u_8} {𝒮 : Type u_9} [Listed m] [Semiring 𝒮] [DecidableEq m] [Fintype m] (M : Matrix m m 𝒮) (i : ℕ) : ofMatrix (M ^ i) = ofMatrix M ^ i

@[simp]

theorem EMatrix.sum_apply {m : Type u_8} {n : Type u_9} {𝒮 : Type u_10} [Listed m] [Listed n] [AddCommMonoid 𝒮] {ι : Type u_11} {S : Finset ι} (f : ι → EMatrix m n 𝒮) {x : m} {y : n} : (∑ i ∈ S, f i) x y = ∑ i ∈ S, (f i) x y

@[simp]

theorem EMatrix.asMatrix_sum {m : Type u_8} {n : Type u_9} {𝒮 : Type u_10} [Listed m] [Listed n] [AddCommMonoid 𝒮] {ι : Type u_11} {S : Finset ι} (f : ι → EMatrix m n 𝒮) : (∑ i ∈ S, f i).asMatrix = ∑ i ∈ S, (f i).asMatrix

@[simp]

theorem EMatrix.ωSum_apply {m : Type u_8} {n : Type u_9} {𝒮 : Type u_10} [Listed m] [Listed n] [AddCommMonoid 𝒮] {ι : Type u_11} [Countable ι] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (f : ι → EMatrix m n 𝒮) {x : m} {y : n} : (ω∑ (i : ι), f i) x y = ω∑ (i : ι), (f i) x y

@[simp]

theorem EMatrix.asMatrix_ωSum {m : Type u_8} {n : Type u_9} {𝒮 : Type u_10} [Listed m] [Listed n] [AddCommMonoid 𝒮] {ι : Type u_11} [Countable ι] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (f : ι → EMatrix m n 𝒮) : (ω∑ (i : ι), f i).asMatrix = ω∑ (i : ι), (f i).asMatrix

@[simp]

theorem EMatrix.asMatrix_ωSum' {m : Type u_8} {n : Type u_9} {𝒮 : Type u_10} [Listed m] [Listed n] [AddCommMonoid 𝒮] {ι : Type u_11} [Countable ι] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (f : ι → NMatrix (Listed.size m) (Listed.size n) 𝒮) : asMatrix (ω∑ (i : ι), f i) = ω∑ (i : ι), asMatrix (f i)