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

Equations

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

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

A column vector

Equations

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

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

A row vector

Equations

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

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

A block matrix

Equations

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

@[implicit_reducible]

instance instOmegaCompletePartialOrderMatrix_weightedNetKAT {𝒮 : Type u_1} [OmegaCompletePartialOrder 𝒮] {X : Type u_2} {Y : Type u_3} : OmegaCompletePartialOrder (Matrix X Y 𝒮)

Equations

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

@[implicit_reducible]

instance instOrderBotMatrix_weightedNetKAT {𝒮 : Type u_1} [OmegaCompletePartialOrder 𝒮] {X : Type u_2} {Y : Type u_3} [OrderBot 𝒮] : OrderBot (Matrix X Y 𝒮)

Equations

• instOrderBotMatrix_weightedNetKAT = { bot := instOrderBotMatrix_weightedNetKAT._aux_1, bot_le := ⋯ }

instance instIsPositiveOrderedAddMonoidMatrix {𝒮 : Type u_1} [OmegaCompletePartialOrder 𝒮] {X : Type u_2} {Y : Type u_3} [OrderBot 𝒮] [AddCommMonoid 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : IsPositiveOrderedAddMonoid (Matrix X Y 𝒮)

theorem Matrix.C_mul_R {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) : A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

Alias of Matrix.fromCols_mul_fromRows.

theorem Matrix.C_mul_B {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) : A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)

Alias of Matrix.fromCols_mul_fromBlocks.

theorem Matrix.B_mul_B {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {q : Type u_6} {α : Type u_12} [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (A' : Matrix l p α) (B' : Matrix l q α) (C' : Matrix m p α) (D' : Matrix m q α) : fromBlocks A B C D * fromBlocks A' B' C' D' = fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')

Alias of Matrix.fromBlocks_multiply.

theorem Matrix.B_mul_R {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix n₁ n R) (A₂ : Matrix n₂ n R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) : fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

Alias of Matrix.fromBlocks_mul_fromRows.

def Matrix.unfold {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} {α : Type u_5} (m : Matrix A B (Matrix C D α)) : Matrix C D (Matrix A B α)

Equations

• m.unfold c d a b = m a b c d

@[simp]

theorem Matrix.unfold_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} {α : Type u_5} (m : Matrix A B (Matrix C D α)) (c : C) (d : D) : m.unfold c d = fun (a : A) (b : B) => m a b c d

def Matrix.down {A : Type u_1} {B : Type u_2} {α : Type u_3} [Unique A] [Unique B] (m : Matrix A B α) : α

Equations

• m.down = m default default

def Matrix.up {A : Type u_1} {B : Type u_2} {α : Type u_3} (a : α) : Matrix A B α

Equations

• ↑a x✝¹ x✝ = a

@[implicit_reducible]

instance Matrix.instCoe_weightedNetKAT {A : Type u_1} {B : Type u_2} {α : Type u_3} : Coe α (Matrix A B α)

Equations

• Matrix.instCoe_weightedNetKAT = { coe := Matrix.up }

@[simp]

theorem Matrix.up_apply {A : Type u_1} {B : Type u_2} {α : Type u_3} (a : α) (x : A) (y : B) : ↑a x y = a

@[simp]

def Matrix.down_up {A : Type u_1} {B : Type u_2} {α : Type u_3} [AddCommMonoid α] [Unique A] [Unique B] (a : α) : (↑a).down = a

Equations

• ⋯ = ⋯

@[simp]

def Matrix.up_down {A : Type u_1} {B : Type u_2} {α : Type u_3} [AddCommMonoid α] [Unique A] [Unique B] (m : Matrix A B α) : ↑m.down = m

Equations

• ⋯ = ⋯

@[simp]

def Matrix.down_sum {ι : Type u_1} {A : Type u_2} {B : Type u_3} {α : Type u_4} [AddCommMonoid α] [Unique A] [Unique B] (f : ι → Matrix A B α) (S : Finset ι) : (∑ x ∈ S, f x).down = ∑ x ∈ S, (f x).down

Equations

• ⋯ = ⋯

@[simp]

def Matrix.down_add {A : Type u_1} {B : Type u_2} {α : Type u_3} [AddCommMonoid α] [Unique A] [Unique B] (m m' : Matrix A B α) : (m + m').down = m.down + m'.down

Equations

• ⋯ = ⋯

@[simp]

def Matrix.down_mul {A : Type u_1} {B : Type u_2} {C : Type u_3} {α : Type u_4} [NonUnitalSemiring α] [Unique A] [Unique B] [Unique C] (m : Matrix A B α) (m' : Matrix B C α) : (m * m').down = m.down * m'.down

Equations

• ⋯ = ⋯

@[simp]

def Matrix.down_mul_right {A : Type u_1} {B : Type u_2} {α : Type u_3} [NonUnitalSemiring α] [Unique A] [Unique B] (m : Matrix A B α) (s : α) : (MulOpposite.op s • m).down = m.down * s

Equations

• ⋯ = ⋯

@[simp]

def Matrix.down_zero {A : Type u_1} {B : Type u_2} {α : Type u_3} [AddCommMonoid α] [Unique A] [Unique B] : down 0 = 0

Equations

• ⋯ = ⋯

@[simp]

def Matrix.down_smul_left {A : Type u_1} {B : Type u_2} {α : Type u_3} [NonUnitalSemiring α] [Unique A] [Unique B] (m : Matrix A B α) (r : α) : (r • m).down = r • m.down

Equations

• ⋯ = ⋯

@[simp]

def Matrix.down_smul_right {A : Type u_1} {B : Type u_2} {α : Type u_3} [NonUnitalSemiring α] [Unique A] [Unique B] (m : Matrix A B α) (r : α) : (MulOpposite.op r • m).down = MulOpposite.op r • m.down

Equations

• ⋯ = ⋯

@[simp]

theorem Matrix.up_add {A : Type u_1} {B : Type u_2} {α : Type u_3} [AddCommMonoid α] (a b : α) : ↑(a + b) = ↑a + ↑b

def Matrix.coe_unique_left {A : Type u_1} {A' : Type u_2} {B : Type u_3} {α : Type u_4} [Unique A] [Unique A'] (m : Matrix A B α) : Matrix A' B α

Equations

• m.coe_unique_left x✝ b = m default b

theorem Matrix.coe_unique_left_fun {A : Type u_1} {A' : Type u_2} {B : Type u_3} {α : Type u_4} [Unique A] [Unique A'] (f : A → B → α) : (coe_unique_left fun (a : A) (b : B) => f a b) = fun (x : A') (b : B) => f default b

@[simp]

theorem Matrix.coe_unique_left_apply {A : Type u_1} {A' : Type u_2} {B : Type u_3} {α : Type u_4} [Unique A] [Unique A'] (f : A → B → α) (a : A') (b : B) : coe_unique_left f a b = f default b

@[simp]

theorem Matrix.coe_unique_left_coe_unique_left {A : Type u_1} {A' : Type u_2} {A'' : Type u_3} {B : Type u_4} {α : Type u_5} [Unique A] [Unique A'] [Unique A''] (f : A → B → α) : (coe_unique_left f).coe_unique_left = coe_unique_left f

@[simp]

theorem Matrix.coe_unique_left_idem {A : Type u_1} {B : Type u_2} {α : Type u_3} [Unique A] (f : A → B → α) : coe_unique_left f = f

@[simp]

theorem Matrix.coe_unique_left_mul {A : Type u_1} {A' : Type u_2} {B : Type u_3} {C : Type u_4} {α : Type u_5} [Unique A] [Unique A'] [DecidableEq A] [Fintype A] [DecidableEq B] [Fintype B] [AddCommMonoid α] [Mul α] (f : Matrix A B α) (g : Matrix B C α) : (f * g).coe_unique_left = f.coe_unique_left * g

@[simp]

theorem Matrix.coe_unique_left_Add {A : Type u_1} {A' : Type u_2} {B : Type u_3} {α : Type u_4} [Unique A] [Unique A'] [DecidableEq A] [Fintype A] [DecidableEq B] [Fintype B] [Add α] (f g : Matrix A B α) : (f + g).coe_unique_left = f.coe_unique_left + g.coe_unique_left

@[simp]

theorem Matrix.coe_unique_left_sum {A : Type u_1} {A' : Type u_2} {B : Type u_3} {ι : Type u_4} {α : Type u_5} [Unique A] [Unique A'] [DecidableEq A] [Fintype A] [DecidableEq B] [Fintype B] [Fintype ι] [DecidableEq ι] [AddCommMonoid α] [Mul α] {S : Finset ι} (f : ι → Matrix A B α) : (∑ i ∈ S, f i).coe_unique_left = ∑ i ∈ S, (f i).coe_unique_left

@[simp]

theorem Matrix.ωSum_apply {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Countable ι] [DecidableEq A] [Fintype A] [DecidableEq B] [Fintype B] {f : ι → Matrix A B 𝒮} (a : A) : (ω∑ (x : ι), f x) a = ω∑ (x : ι), f x a

@[simp]

theorem Matrix.up_ωSum {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {ι : Type u_2} {A : Type u_3} {N : Type u_4} [Countable ι] [DecidableEq A] [Fintype A] [DecidableEq N] [Fintype N] {f : ι → Matrix A A 𝒮} : ↑(ω∑ (x : ι), f x) = ω∑ (x : ι), ↑(f x)

theorem Matrix.of_ωSum {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Countable ι] [DecidableEq A] [Fintype A] [DecidableEq B] [Fintype B] {f : ι → Matrix A B 𝒮} : (of fun (a : A) (b : B) => ω∑ (x : ι), f x a b) = ω∑ (x : ι), of fun (a : A) (b : B) => f x a b

theorem Matrix.of_ωSum' {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Countable ι] [DecidableEq A] [Fintype A] [DecidableEq B] [Fintype B] {f : ι → Matrix A B 𝒮} : (fun (a : A) (b : B) => ω∑ (x : ι), f x a b) = ω∑ (x : ι), fun (a : A) (b : B) => f x a b

theorem Matrix.ωSum_mul_right {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {ι : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Countable ι] [DecidableEq A] [Fintype A] [DecidableEq B] [Fintype B] [DecidableEq C] [Fintype C] {f : ι → Matrix A B 𝒮} (a : Matrix B C 𝒮) : ω∑ (x : ι), f x * a = (ω∑ (x : ι), f x) * a

theorem Matrix.ωSum_mul_left {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {ι : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Countable ι] [DecidableEq A] [Fintype A] [DecidableEq B] [Fintype B] [DecidableEq C] [Fintype C] {f : ι → Matrix B C 𝒮} (a : Matrix A B 𝒮) : ω∑ (x : ι), a * f x = a * ω∑ (x : ι), f x

instance Matrix.instMulLeftMonoOfDecidableEq_weightedNetKAT {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] {N : Type u_2} [DecidableEq N] [Fintype N] : MulLeftMono (Matrix N N 𝒮)

instance Matrix.instMulRightMonoOfDecidableEq_weightedNetKAT {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulRightMono 𝒮] {N : Type u_2} [DecidableEq N] [Fintype N] : MulRightMono (Matrix N N 𝒮)

instance Matrix.instOmegaContinuousNonUnitalSemiring {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {N : Type u_2} [DecidableEq N] [Fintype N] : OmegaContinuousNonUnitalSemiring (Matrix N N 𝒮)

@[simp]

theorem Matrix.fun_one_mul {𝒮 : Type u_1} {m : Type u_2} {n : Type u_3} [Semiring 𝒮] [Fintype m] [Unique m] (x : Matrix m n 𝒮) : (fun (x : m) => 1) * x = x

@[simp]

theorem Matrix.mul_fun_one {𝒮 : Type u_1} {m : Type u_2} {n : Type u_3} [Semiring 𝒮] [Fintype n] [Unique n] (x : Matrix m n 𝒮) : (x * fun (x : n) => 1) = x

theorem Matrix.unit_mul_apply {α : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommMonoid α] [Mul α] (A : Matrix X Unit α) (B : Matrix Unit Y α) (x : X) (y : Y) : (A * B) x y = A x () * B () y

@[simp]

theorem Matrix.smul_apply' {α : Type u_1} {X : Type u_2} [AddCommMonoid α] [Mul α] (r : α) (A : Matrix X X α) (i j : X) : (MulOpposite.op r • A) i j = A i j • r