Matrices

This file defines basic properties of matrices.

Matrices with rows indexed by m, columns indexed by n, and entries of type α are represented with Matrix m n α. For the typical approach of counting rows and columns, Matrix (Fin m) (Fin n) α can be used.

Notation

The locale Matrix gives the following notation:

• ⬝ᵥ for Matrix.dotProduct
• *ᵥ for Matrix.mulVec
• ᵥ* for Matrix.vecMul
• ᵀ for Matrix.transpose
• ᴴ for Matrix.conjTranspose

Implementation notes

For convenience, Matrix m n α is defined as m → n → α, as this allows elements of the matrix to be accessed with A i j. However, it is not advisable to construct matrices using terms of the form fun i j ↦ _ or even (fun i j ↦ _ : Matrix m n α), as these are not recognized by Lean as having the right type. Instead, Matrix.of should be used.

TODO

Under various conditions, multiplication of infinite matrices makes sense. These have not yet been implemented.

def Matrix (m : Type u) (n : Type u') (α : Type v) : Type (max u u' v)

Matrix m n R is the type of matrices with entries in R, whose rows are indexed by m and whose columns are indexed by n.

Equations

• Matrix m n α = (m → n → α)

theorem Matrix.ext_iff {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {N : Matrix m n α} : (∀ (i : m) (j : n), M i j = N i j) ↔ M = N

theorem Matrix.ext {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {N : Matrix m n α} : (∀ (i : m) (j : n), M i j = N i j) → M = N

def Matrix.of {m : Type u_2} {n : Type u_3} {α : Type v} : (m → n → α) ≃ Matrix m n α

Cast a function into a matrix.

The two sides of the equivalence are definitionally equal types. We want to use an explicit cast to distinguish the types because Matrix has different instances to pi types (such as Pi.mul, which performs elementwise multiplication, vs Matrix.mul).

If you are defining a matrix, in terms of its entries, use of (fun i j ↦ _). The purpose of this approach is to ensure that terms of the form (fun i j ↦ _) * (fun i j ↦ _) do not appear, as the type of * can be misleading.

Porting note: In Lean 3, it is also safe to use pattern matching in a definition as | i j := _, which can only be unfolded when fully-applied. leanprover/lean4#2042 means this does not (currently) work in Lean 4.

Equations

• Matrix.of = Equiv.refl (m → n → α)

@[simp]

theorem Matrix.of_apply {m : Type u_2} {n : Type u_3} {α : Type v} (f : m → n → α) (i : m) (j : n) : Matrix.of f i j = f i j

@[simp]

theorem Matrix.of_symm_apply {m : Type u_2} {n : Type u_3} {α : Type v} (f : Matrix m n α) (i : m) (j : n) : Matrix.of.symm f i j = f i j

def Matrix.map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (M : Matrix m n α) (f : α → β) : Matrix m n β

M.map f is the matrix obtained by applying f to each entry of the matrix M.

This is available in bundled forms as:

• AddMonoidHom.mapMatrix
• LinearMap.mapMatrix
• RingHom.mapMatrix
• AlgHom.mapMatrix
• Equiv.mapMatrix
• AddEquiv.mapMatrix
• LinearEquiv.mapMatrix
• RingEquiv.mapMatrix
• AlgEquiv.mapMatrix

Equations

• M.map f = Matrix.of fun (i : m) (j : n) => f (M i j)

@[simp]

theorem Matrix.map_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {f : α → β} {i : m} {j : n} : M.map f i j = f (M i j)

@[simp]

theorem Matrix.map_id {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) : M.map id = M

@[simp]

theorem Matrix.map_id' {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) : (M.map fun (x : α) => x) = M

@[simp]

theorem Matrix.map_map {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {β : Type u_10} {γ : Type u_11} {f : α → β} {g : β → γ} : (M.map f).map g = M.map (g ∘ f)

theorem Matrix.map_injective {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} (hf : Function.Injective f) : Function.Injective fun (M : Matrix m n α) => M.map f

def Matrix.transpose {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) : Matrix n m α

The transpose of a matrix.

Equations

• M.transpose = Matrix.of fun (x : n) (y : m) => M y x

@[simp]

theorem Matrix.transpose_apply {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) (i : n) (j : m) : M.transpose i j = M j i

def Matrix.«term_ᵀ» : Lean.TrailingParserDescr

The transpose of a matrix.

Equations

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

def Matrix.conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} [Star α] (M : Matrix m n α) : Matrix n m α

The conjugate transpose of a matrix defined in term of star.

Equations

• M.conjTranspose = M.transpose.map star

def Matrix.«term_ᴴ» : Lean.TrailingParserDescr

The conjugate transpose of a matrix defined in term of star.

Equations

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

instance Matrix.inhabited {m : Type u_2} {n : Type u_3} {α : Type v} [Inhabited α] : Inhabited (Matrix m n α)

Equations

• Matrix.inhabited = inferInstanceAs (Inhabited (m → n → α))

instance Matrix.decidableEq {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq α] [Fintype m] [Fintype n] : DecidableEq (Matrix m n α)

Equations

• Matrix.decidableEq = Fintype.decidablePiFintype

instance Matrix.instFintypeOfDecidableEq {n : Type u_10} {m : Type u_11} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (α : Type u_12) [Fintype α] : Fintype (Matrix m n α)

Equations

• Matrix.instFintypeOfDecidableEq α = inferInstanceAs (Fintype (m → n → α))

instance Matrix.instFinite {n : Type u_10} {m : Type u_11} [Finite m] [Finite n] (α : Type u_12) [Finite α] : Finite (Matrix m n α)

Equations

• ⋯ = ⋯

instance Matrix.add {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] : Add (Matrix m n α)

Equations

• Matrix.add = Pi.instAdd

instance Matrix.addSemigroup {m : Type u_2} {n : Type u_3} {α : Type v} [AddSemigroup α] : AddSemigroup (Matrix m n α)

Equations

• Matrix.addSemigroup = Pi.addSemigroup

instance Matrix.addCommSemigroup {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommSemigroup α] : AddCommSemigroup (Matrix m n α)

Equations

• Matrix.addCommSemigroup = Pi.addCommSemigroup

instance Matrix.zero {m : Type u_2} {n : Type u_3} {α : Type v} [Zero α] : Zero (Matrix m n α)

Equations

• Matrix.zero = Pi.instZero

instance Matrix.addZeroClass {m : Type u_2} {n : Type u_3} {α : Type v} [AddZeroClass α] : AddZeroClass (Matrix m n α)

Equations

• Matrix.addZeroClass = Pi.addZeroClass

instance Matrix.addMonoid {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] : AddMonoid (Matrix m n α)

Equations

• Matrix.addMonoid = Pi.addMonoid

instance Matrix.addCommMonoid {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommMonoid α] : AddCommMonoid (Matrix m n α)

Equations

• Matrix.addCommMonoid = Pi.addCommMonoid

instance Matrix.neg {m : Type u_2} {n : Type u_3} {α : Type v} [Neg α] : Neg (Matrix m n α)

Equations

• Matrix.neg = Pi.instNeg

instance Matrix.sub {m : Type u_2} {n : Type u_3} {α : Type v} [Sub α] : Sub (Matrix m n α)

Equations

• Matrix.sub = Pi.instSub

instance Matrix.addGroup {m : Type u_2} {n : Type u_3} {α : Type v} [AddGroup α] : AddGroup (Matrix m n α)

Equations

• Matrix.addGroup = Pi.addGroup

instance Matrix.addCommGroup {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommGroup α] : AddCommGroup (Matrix m n α)

Equations

• Matrix.addCommGroup = Pi.addCommGroup

instance Matrix.unique {m : Type u_2} {n : Type u_3} {α : Type v} [Unique α] : Unique (Matrix m n α)

Equations

• Matrix.unique = Pi.unique

instance Matrix.subsingleton {m : Type u_2} {n : Type u_3} {α : Type v} [Subsingleton α] : Subsingleton (Matrix m n α)

Equations

• ⋯ = ⋯

instance Matrix.nonempty {m : Type u_2} {n : Type u_3} {α : Type v} [Nonempty m] [Nonempty n] [Nontrivial α] : Nontrivial (Matrix m n α)

Equations

• ⋯ = ⋯

instance Matrix.smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [SMul R α] : SMul R (Matrix m n α)

Equations

• Matrix.smul = Pi.instSMul

instance Matrix.smulCommClass {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type v} [SMul R α] [SMul S α] [SMulCommClass R S α] : SMulCommClass R S (Matrix m n α)

Equations

• ⋯ = ⋯

instance Matrix.isScalarTower {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type v} [SMul R S] [SMul R α] [SMul S α] [IsScalarTower R S α] : IsScalarTower R S (Matrix m n α)

Equations

• ⋯ = ⋯

instance Matrix.isCentralScalar {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] : IsCentralScalar R (Matrix m n α)

Equations

• ⋯ = ⋯

instance Matrix.mulAction {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Monoid R] [MulAction R α] : MulAction R (Matrix m n α)

Equations

• Matrix.mulAction = Pi.mulAction R

instance Matrix.distribMulAction {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Monoid R] [AddMonoid α] [DistribMulAction R α] : DistribMulAction R (Matrix m n α)

Equations

• Matrix.distribMulAction = Pi.distribMulAction R

instance Matrix.module {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Semiring R] [AddCommMonoid α] [Module R α] : Module R (Matrix m n α)

Equations

• Matrix.module = Pi.module m (fun (a : m) => n → α) R

@[simp]

theorem Matrix.zero_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Zero α] (i : m) (j : n) : 0 i j = 0

@[simp]

theorem Matrix.add_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] (A : Matrix m n α) (B : Matrix m n α) (i : m) (j : n) : (A + B) i j = A i j + B i j

@[simp]

theorem Matrix.smul_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [SMul β α] (r : β) (A : Matrix m n α) (i : m) (j : n) : (r • A) i j = r • A i j

@[simp]

theorem Matrix.sub_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Sub α] (A : Matrix m n α) (B : Matrix m n α) (i : m) (j : n) : (A - B) i j = A i j - B i j

@[simp]

theorem Matrix.neg_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Neg α] (A : Matrix m n α) (i : m) (j : n) : (-A) i j = -A i j

simp-normal form pulls of to the outside.

@[simp]

theorem Matrix.of_zero {m : Type u_2} {n : Type u_3} {α : Type v} [Zero α] : Matrix.of 0 = 0

@[simp]

theorem Matrix.of_add_of {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] (f : m → n → α) (g : m → n → α) : Matrix.of f + Matrix.of g = Matrix.of (f + g)

@[simp]

theorem Matrix.of_sub_of {m : Type u_2} {n : Type u_3} {α : Type v} [Sub α] (f : m → n → α) (g : m → n → α) : Matrix.of f - Matrix.of g = Matrix.of (f - g)

@[simp]

theorem Matrix.neg_of {m : Type u_2} {n : Type u_3} {α : Type v} [Neg α] (f : m → n → α) : -Matrix.of f = Matrix.of (-f)

@[simp]

theorem Matrix.smul_of {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [SMul R α] (r : R) (f : m → n → α) : r • Matrix.of f = Matrix.of (r • f)

@[simp]

theorem Matrix.map_zero {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Zero α] [Zero β] (f : α → β) (h : f 0 = 0) : Matrix.map 0 f = 0

theorem Matrix.map_add {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Add α] [Add β] (f : α → β) (hf : ∀ (a₁ a₂ : α), f (a₁ + a₂) = f a₁ + f a₂) (M : Matrix m n α) (N : Matrix m n α) : (M + N).map f = M.map f + N.map f

theorem Matrix.map_sub {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Sub α] [Sub β] (f : α → β) (hf : ∀ (a₁ a₂ : α), f (a₁ - a₂) = f a₁ - f a₂) (M : Matrix m n α) (N : Matrix m n α) : (M - N).map f = M.map f - N.map f

theorem Matrix.map_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [SMul R α] [SMul R β] (f : α → β) (r : R) (hf : ∀ (a : α), f (r • a) = r • f a) (M : Matrix m n α) : (r • M).map f = r • M.map f

theorem Matrix.map_smul' {n : Type u_3} {α : Type v} {β : Type w} [Mul α] [Mul β] (f : α → β) (r : α) (A : Matrix n n α) (hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) : (r • A).map f = f r • A.map f

The scalar action via Mul.toSMul is transformed by the same map as the elements of the matrix, when f preserves multiplication.

theorem Matrix.map_op_smul' {n : Type u_3} {α : Type v} {β : Type w} [Mul α] [Mul β] (f : α → β) (r : α) (A : Matrix n n α) (hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) : (MulOpposite.op r • A).map f = MulOpposite.op (f r) • A.map f

The scalar action via mul.toOppositeSMul is transformed by the same map as the elements of the matrix, when f preserves multiplication.

theorem IsSMulRegular.matrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [SMul R S] {k : R} (hk : IsSMulRegular S k) : IsSMulRegular (Matrix m n S) k

theorem IsLeftRegular.matrix {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] {k : α} (hk : IsLeftRegular k) : IsSMulRegular (Matrix m n α) k

instance Matrix.subsingleton_of_empty_left {m : Type u_2} {n : Type u_3} {α : Type v} [IsEmpty m] : Subsingleton (Matrix m n α)

Equations

• ⋯ = ⋯

instance Matrix.subsingleton_of_empty_right {m : Type u_2} {n : Type u_3} {α : Type v} [IsEmpty n] : Subsingleton (Matrix m n α)

Equations

• ⋯ = ⋯

def Matrix.diagonal {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) : Matrix n n α

diagonal d is the square matrix such that (diagonal d) i i = d i and (diagonal d) i j = 0 if i ≠ j.

Note that bundled versions exist as:

• Matrix.diagonalAddMonoidHom
• Matrix.diagonalLinearMap
• Matrix.diagonalRingHom
• Matrix.diagonalAlgHom

Equations

• Matrix.diagonal d = Matrix.of fun (i j : n) => if i = j then d i else 0

theorem Matrix.diagonal_apply {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) (i : n) (j : n) : Matrix.diagonal d i j = if i = j then d i else 0

@[simp]

theorem Matrix.diagonal_apply_eq {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) (i : n) : Matrix.diagonal d i i = d i

@[simp]

theorem Matrix.diagonal_apply_ne {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) {i : n} {j : n} (h : i ≠ j) : Matrix.diagonal d i j = 0

theorem Matrix.diagonal_apply_ne' {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) {i : n} {j : n} (h : j ≠ i) : Matrix.diagonal d i j = 0

@[simp]

theorem Matrix.diagonal_eq_diagonal_iff {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] {d₁ : n → α} {d₂ : n → α} : Matrix.diagonal d₁ = Matrix.diagonal d₂ ↔ ∀ (i : n), d₁ i = d₂ i

theorem Matrix.diagonal_injective {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] : Function.Injective Matrix.diagonal

@[simp]

theorem Matrix.diagonal_zero {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] : (Matrix.diagonal fun (x : n) => 0) = 0

@[simp]

theorem Matrix.diagonal_transpose {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (v : n → α) : (Matrix.diagonal v).transpose = Matrix.diagonal v

@[simp]

theorem Matrix.diagonal_add {n : Type u_3} {α : Type v} [DecidableEq n] [AddZeroClass α] (d₁ : n → α) (d₂ : n → α) : Matrix.diagonal d₁ + Matrix.diagonal d₂ = Matrix.diagonal fun (i : n) => d₁ i + d₂ i

@[simp]

theorem Matrix.diagonal_smul {n : Type u_3} {R : Type u_7} {α : Type v} [DecidableEq n] [Zero α] [SMulZeroClass R α] (r : R) (d : n → α) : Matrix.diagonal (r • d) = r • Matrix.diagonal d

@[simp]

theorem Matrix.diagonal_neg {n : Type u_3} {α : Type v} [DecidableEq n] [NegZeroClass α] (d : n → α) : -Matrix.diagonal d = Matrix.diagonal fun (i : n) => -d i

@[simp]

theorem Matrix.diagonal_sub {n : Type u_3} {α : Type v} [DecidableEq n] [SubNegZeroMonoid α] (d₁ : n → α) (d₂ : n → α) : Matrix.diagonal d₁ - Matrix.diagonal d₂ = Matrix.diagonal fun (i : n) => d₁ i - d₂ i

instance Matrix.instNatCastOfZero {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] : NatCast (Matrix n n α)

Equations

• Matrix.instNatCastOfZero = { natCast := fun (m : ℕ) => Matrix.diagonal fun (x : n) => ↑m }

theorem Matrix.diagonal_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] (m : ℕ) : (Matrix.diagonal fun (x : n) => ↑m) = ↑m

theorem Matrix.diagonal_natCast' {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] (m : ℕ) : Matrix.diagonal ↑m = ↑m

theorem Matrix.diagonal_ofNat {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] : (Matrix.diagonal fun (x : n) => OfNat.ofNat m) = OfNat.ofNat m

theorem Matrix.diagonal_ofNat' {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] : Matrix.diagonal (OfNat.ofNat m) = OfNat.ofNat m

instance Matrix.instIntCastOfZero {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [IntCast α] : IntCast (Matrix n n α)

Equations

• Matrix.instIntCastOfZero = { intCast := fun (m : ℤ) => Matrix.diagonal fun (x : n) => ↑m }

theorem Matrix.diagonal_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [IntCast α] (m : ℤ) : (Matrix.diagonal fun (x : n) => ↑m) = ↑m

theorem Matrix.diagonal_intCast' {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [IntCast α] (m : ℤ) : Matrix.diagonal ↑m = ↑m

@[simp]

theorem Matrix.diagonalAddMonoidHom_apply (n : Type u_3) (α : Type v) [DecidableEq n] [AddZeroClass α] (d : n → α) : (Matrix.diagonalAddMonoidHom n α) d = Matrix.diagonal d

def Matrix.diagonalAddMonoidHom (n : Type u_3) (α : Type v) [DecidableEq n] [AddZeroClass α] : (n → α) →+ Matrix n n α

Matrix.diagonal as an AddMonoidHom.

Equations

• Matrix.diagonalAddMonoidHom n α = { toFun := Matrix.diagonal, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.diagonalLinearMap_apply (n : Type u_3) (R : Type u_7) (α : Type v) [DecidableEq n] [Semiring R] [AddCommMonoid α] [Module R α] : ∀ (a : n → α), (Matrix.diagonalLinearMap n R α) a = (↑(Matrix.diagonalAddMonoidHom n α)).toFun a

def Matrix.diagonalLinearMap (n : Type u_3) (R : Type u_7) (α : Type v) [DecidableEq n] [Semiring R] [AddCommMonoid α] [Module R α] : (n → α) →ₗ[R] Matrix n n α

Matrix.diagonal as a LinearMap.

Equations

• Matrix.diagonalLinearMap n R α = let __src := Matrix.diagonalAddMonoidHom n α; { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Matrix.diagonal_map {n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [Zero α] [Zero β] {f : α → β} (h : f 0 = 0) {d : n → α} : (Matrix.diagonal d).map f = Matrix.diagonal fun (m : n) => f (d m)

theorem Matrix.map_natCast {n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [AddMonoidWithOne α] [AddMonoidWithOne β] {f : α → β} (h : f 0 = 0) (d : ℕ) : (↑d).map f = Matrix.diagonal fun (x : n) => f ↑d

theorem Matrix.map_ofNat {n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [AddMonoidWithOne α] [AddMonoidWithOne β] {f : α → β} (h : f 0 = 0) (d : ℕ) [d.AtLeastTwo] : (OfNat.ofNat d).map f = Matrix.diagonal fun (x : n) => f (OfNat.ofNat d)

theorem Matrix.map_intCast {n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [AddGroupWithOne α] [AddGroupWithOne β] {f : α → β} (h : f 0 = 0) (d : ℤ) : (↑d).map f = Matrix.diagonal fun (x : n) => f ↑d

@[simp]

theorem Matrix.diagonal_conjTranspose {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoid α] [StarAddMonoid α] (v : n → α) : (Matrix.diagonal v).conjTranspose = Matrix.diagonal (star v)

instance Matrix.one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] : One (Matrix n n α)

Equations

• Matrix.one = { one := Matrix.diagonal fun (x : n) => 1 }

@[simp]

theorem Matrix.diagonal_one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] : (Matrix.diagonal fun (x : n) => 1) = 1

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

@[simp]

theorem Matrix.one_apply_eq {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] (i : n) : 1 i i = 1

@[simp]

theorem Matrix.one_apply_ne {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] {i : n} {j : n} : i ≠ j → 1 i j = 0

theorem Matrix.one_apply_ne' {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] {i : n} {j : n} : j ≠ i → 1 i j = 0

@[simp]

theorem Matrix.map_one {n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [Zero α] [One α] [Zero β] [One β] (f : α → β) (h₀ : f 0 = 0) (h₁ : f 1 = 1) : Matrix.map 1 f = 1

theorem Matrix.one_eq_pi_single {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] {i : n} {j : n} : 1 i j = Pi.single i 1 j

theorem Matrix.zero_le_one_elem {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] [Preorder α] [ZeroLEOneClass α] (i : n) (j : n) : 0 ≤ 1 i j

theorem Matrix.zero_le_one_row {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] [Preorder α] [ZeroLEOneClass α] (i : n) : 0 ≤ 1 i

instance Matrix.instAddMonoidWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] : AddMonoidWithOne (Matrix n n α)

Equations

• Matrix.instAddMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯

instance Matrix.instAddGroupWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddGroupWithOne α] : AddGroupWithOne (Matrix n n α)

Equations

• Matrix.instAddGroupWithOne = let __spread.0 := Matrix.addGroup; let __spread.1 := Matrix.instAddMonoidWithOne; AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Matrix.instAddCommMonoidWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddCommMonoidWithOne α] : AddCommMonoidWithOne (Matrix n n α)

Equations

• Matrix.instAddCommMonoidWithOne = let __spread.0 := Matrix.addCommMonoid; let __spread.1 := Matrix.instAddMonoidWithOne; AddCommMonoidWithOne.mk ⋯

instance Matrix.instAddCommGroupWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddCommGroupWithOne α] : AddCommGroupWithOne (Matrix n n α)

Equations

• Matrix.instAddCommGroupWithOne = let __spread.0 := Matrix.addCommGroup; let __spread.1 := Matrix.instAddGroupWithOne; AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯

def Matrix.diag {n : Type u_3} {α : Type v} (A : Matrix n n α) (i : n) : α

The diagonal of a square matrix.

Equations

• A.diag i = A i i

@[simp]

theorem Matrix.diag_apply {n : Type u_3} {α : Type v} (A : Matrix n n α) (i : n) : A.diag i = A i i

@[simp]

theorem Matrix.diag_diagonal {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (a : n → α) : (Matrix.diagonal a).diag = a

@[simp]

theorem Matrix.diag_transpose {n : Type u_3} {α : Type v} (A : Matrix n n α) : A.transpose.diag = A.diag

@[simp]

theorem Matrix.diag_zero {n : Type u_3} {α : Type v} [Zero α] : Matrix.diag 0 = 0

@[simp]

theorem Matrix.diag_add {n : Type u_3} {α : Type v} [Add α] (A : Matrix n n α) (B : Matrix n n α) : (A + B).diag = A.diag + B.diag

@[simp]

theorem Matrix.diag_sub {n : Type u_3} {α : Type v} [Sub α] (A : Matrix n n α) (B : Matrix n n α) : (A - B).diag = A.diag - B.diag

@[simp]

theorem Matrix.diag_neg {n : Type u_3} {α : Type v} [Neg α] (A : Matrix n n α) : (-A).diag = -A.diag

@[simp]

theorem Matrix.diag_smul {n : Type u_3} {R : Type u_7} {α : Type v} [SMul R α] (r : R) (A : Matrix n n α) : (r • A).diag = r • A.diag

@[simp]

theorem Matrix.diag_one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] : Matrix.diag 1 = 1

@[simp]

theorem Matrix.diagAddMonoidHom_apply (n : Type u_3) (α : Type v) [AddZeroClass α] (A : Matrix n n α) (i : n) : (Matrix.diagAddMonoidHom n α) A i = A.diag i

def Matrix.diagAddMonoidHom (n : Type u_3) (α : Type v) [AddZeroClass α] : Matrix n n α →+ n → α

Matrix.diag as an AddMonoidHom.

Equations

• Matrix.diagAddMonoidHom n α = { toFun := Matrix.diag, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.diagLinearMap_apply (n : Type u_3) (R : Type u_7) (α : Type v) [Semiring R] [AddCommMonoid α] [Module R α] : ∀ (a : Matrix n n α) (a_1 : n), (Matrix.diagLinearMap n R α) a a_1 = (↑(Matrix.diagAddMonoidHom n α)).toFun a a_1

def Matrix.diagLinearMap (n : Type u_3) (R : Type u_7) (α : Type v) [Semiring R] [AddCommMonoid α] [Module R α] : Matrix n n α →ₗ[R] n → α

Matrix.diag as a LinearMap.

Equations

• Matrix.diagLinearMap n R α = let __src := Matrix.diagAddMonoidHom n α; { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }

theorem Matrix.diag_map {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {A : Matrix n n α} : (A.map f).diag = f ∘ A.diag

@[simp]

theorem Matrix.diag_conjTranspose {n : Type u_3} {α : Type v} [AddMonoid α] [StarAddMonoid α] (A : Matrix n n α) : A.conjTranspose.diag = star A.diag

@[simp]

theorem Matrix.diag_list_sum {n : Type u_3} {α : Type v} [AddMonoid α] (l : List (Matrix n n α)) : l.sum.diag = (List.map Matrix.diag l).sum

@[simp]

theorem Matrix.diag_multiset_sum {n : Type u_3} {α : Type v} [AddCommMonoid α] (s : Multiset (Matrix n n α)) : s.sum.diag = (Multiset.map Matrix.diag s).sum

@[simp]

theorem Matrix.diag_sum {n : Type u_3} {α : Type v} {ι : Type u_10} [AddCommMonoid α] (s : Finset ι) (f : ι → Matrix n n α) : (∑ i ∈ s, f i).diag = ∑ i ∈ s, (f i).diag

def Matrix.dotProduct {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v : m → α) (w : m → α) : α

dotProduct v w is the sum of the entrywise products v i * w i

Equations

• Matrix.dotProduct v w = ∑ i : m, v i * w i

def Matrix.«term_⬝ᵥ_» : Lean.TrailingParserDescr

dotProduct v w is the sum of the entrywise products v i * w i

Equations

• Matrix.«term_⬝ᵥ_» = Lean.ParserDescr.trailingNode `Matrix.term_⬝ᵥ_ 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⬝ᵥ ") (Lean.ParserDescr.cat `term 73))

theorem Matrix.dotProduct_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalSemiring α] (u : m → α) (w : n → α) (v : Matrix m n α) : Matrix.dotProduct (fun (j : n) => Matrix.dotProduct u fun (i : m) => v i j) w = Matrix.dotProduct u fun (i : m) => Matrix.dotProduct (v i) w

theorem Matrix.dotProduct_comm {m : Type u_2} {α : Type v} [Fintype m] [AddCommMonoid α] [CommSemigroup α] (v : m → α) (w : m → α) : Matrix.dotProduct v w = Matrix.dotProduct w v

@[simp]

theorem Matrix.dotProduct_pUnit {α : Type v} [AddCommMonoid α] [Mul α] (v : PUnit.{u_10 + 1} → α) (w : PUnit.{u_10 + 1} → α) : Matrix.dotProduct v w = v PUnit.unit * w PUnit.unit

theorem Matrix.dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : n → α) : Matrix.dotProduct v 1 = ∑ i : n, v i

theorem Matrix.one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : n → α) : Matrix.dotProduct 1 v = ∑ i : n, v i

@[simp]

theorem Matrix.dotProduct_zero {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : Matrix.dotProduct v 0 = 0

@[simp]

theorem Matrix.dotProduct_zero' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : (Matrix.dotProduct v fun (x : m) => 0) = 0

@[simp]

theorem Matrix.zero_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : Matrix.dotProduct 0 v = 0

@[simp]

theorem Matrix.zero_dotProduct' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : Matrix.dotProduct (fun (x : m) => 0) v = 0

@[simp]

theorem Matrix.add_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u : m → α) (v : m → α) (w : m → α) : Matrix.dotProduct (u + v) w = Matrix.dotProduct u w + Matrix.dotProduct v w

@[simp]

theorem Matrix.dotProduct_add {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u : m → α) (v : m → α) (w : m → α) : Matrix.dotProduct u (v + w) = Matrix.dotProduct u v + Matrix.dotProduct u w

@[simp]

theorem Matrix.sum_elim_dotProduct_sum_elim {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : m → α) (v : m → α) (x : n → α) (y : n → α) : Matrix.dotProduct (Sum.elim u x) (Sum.elim v y) = Matrix.dotProduct u v + Matrix.dotProduct x y

@[simp]

theorem Matrix.comp_equiv_symm_dotProduct {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : m → α) (x : n → α) (e : m ≃ n) : Matrix.dotProduct (u ∘ ⇑e.symm) x = Matrix.dotProduct u (x ∘ ⇑e)

Permuting a vector on the left of a dot product can be transferred to the right.

@[simp]

theorem Matrix.dotProduct_comp_equiv_symm {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : m → α) (x : n → α) (e : n ≃ m) : Matrix.dotProduct u (x ∘ ⇑e.symm) = Matrix.dotProduct (u ∘ ⇑e) x

Permuting a vector on the right of a dot product can be transferred to the left.

@[simp]

theorem Matrix.comp_equiv_dotProduct_comp_equiv {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (x : n → α) (y : n → α) (e : m ≃ n) : Matrix.dotProduct (x ∘ ⇑e) (y ∘ ⇑e) = Matrix.dotProduct x y

Permuting vectors on both sides of a dot product is a no-op.

@[simp]

theorem Matrix.diagonal_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (w : m → α) (i : m) : Matrix.dotProduct (Matrix.diagonal v i) w = v i * w i

@[simp]

theorem Matrix.dotProduct_diagonal {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (w : m → α) (i : m) : Matrix.dotProduct v (Matrix.diagonal w i) = v i * w i

@[simp]

theorem Matrix.dotProduct_diagonal' {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (w : m → α) (i : m) : (Matrix.dotProduct v fun (j : m) => Matrix.diagonal w j i) = v i * w i

@[simp]

theorem Matrix.single_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (x : α) (i : m) : Matrix.dotProduct (Pi.single i x) v = x * v i

@[simp]

theorem Matrix.dotProduct_single {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (x : α) (i : m) : Matrix.dotProduct v (Pi.single i x) = v i * x

@[simp]

theorem Matrix.one_dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] : Matrix.dotProduct 1 1 = ↑(Fintype.card n)

@[simp]

theorem Matrix.neg_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v : m → α) (w : m → α) : Matrix.dotProduct (-v) w = -Matrix.dotProduct v w

@[simp]

theorem Matrix.dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v : m → α) (w : m → α) : Matrix.dotProduct v (-w) = -Matrix.dotProduct v w

theorem Matrix.neg_dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v : m → α) (w : m → α) : Matrix.dotProduct (-v) (-w) = Matrix.dotProduct v w

@[simp]

theorem Matrix.sub_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u : m → α) (v : m → α) (w : m → α) : Matrix.dotProduct (u - v) w = Matrix.dotProduct u w - Matrix.dotProduct v w

@[simp]

theorem Matrix.dotProduct_sub {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u : m → α) (v : m → α) (w : m → α) : Matrix.dotProduct u (v - w) = Matrix.dotProduct u v - Matrix.dotProduct u w

@[simp]

theorem Matrix.smul_dotProduct {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [Monoid R] [Mul α] [AddCommMonoid α] [DistribMulAction R α] [IsScalarTower R α α] (x : R) (v : m → α) (w : m → α) : Matrix.dotProduct (x • v) w = x • Matrix.dotProduct v w

@[simp]

theorem Matrix.dotProduct_smul {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [Monoid R] [Mul α] [AddCommMonoid α] [DistribMulAction R α] [SMulCommClass R α α] (x : R) (v : m → α) (w : m → α) : Matrix.dotProduct v (x • w) = x • Matrix.dotProduct v w

theorem Matrix.star_dotProduct_star {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalSemiring α] [StarRing α] (v : m → α) (w : m → α) : Matrix.dotProduct (star v) (star w) = star (Matrix.dotProduct w v)

theorem Matrix.star_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalSemiring α] [StarRing α] (v : m → α) (w : m → α) : Matrix.dotProduct (star v) w = star (Matrix.dotProduct (star w) v)

theorem Matrix.dotProduct_star {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalSemiring α] [StarRing α] (v : m → α) (w : m → α) : Matrix.dotProduct v (star w) = star (Matrix.dotProduct w (star v))

@[defaultInstance 100]

instance Matrix.instHMulOfFintypeOfMulOfAddCommMonoid {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] : HMul (Matrix l m α) (Matrix m n α) (Matrix l n α)

M * N is the usual product of matrices M and N, i.e. we have that (M * N) i k is the dot product of the i-th row of M by the k-th column of N. This is currently only defined when m is finite.

Equations

• Matrix.instHMulOfFintypeOfMulOfAddCommMonoid = { hMul := fun (M : Matrix l m α) (N : Matrix m n α) (i : l) (k : n) => Matrix.dotProduct (fun (j : m) => M i j) fun (j : m) => N j k }

theorem Matrix.mul_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i : l} {k : n} : (M * N) i k = ∑ j : m, M i j * N j k

instance Matrix.instMulOfFintypeOfAddCommMonoid {n : Type u_3} {α : Type v} [Fintype n] [Mul α] [AddCommMonoid α] : Mul (Matrix n n α)

Equations

• Matrix.instMulOfFintypeOfAddCommMonoid = { mul := fun (M N : Matrix n n α) => M * N }

theorem Matrix.mul_apply' {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i : l} {k : n} : (M * N) i k = Matrix.dotProduct (fun (j : m) => M i j) fun (j : m) => N j k

theorem Matrix.sum_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [AddCommMonoid α] (i : m) (j : n) (s : Finset β) (g : β → Matrix m n α) : (∑ c ∈ s, g c) i j = ∑ c ∈ s, g c i j

theorem Matrix.two_mul_expl {R : Type u_10} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R) (B : Matrix (Fin 2) (Fin 2) R) : (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧ (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧ (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

@[simp]

theorem Matrix.smul_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [AddCommMonoid α] [Mul α] [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] (a : R) (M : Matrix m n α) (N : Matrix n l α) : a • M * N = a • (M * N)

@[simp]

theorem Matrix.mul_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [AddCommMonoid α] [Mul α] [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α] (M : Matrix m n α) (a : R) (N : Matrix n l α) : M * a • N = a • (M * N)

@[simp]

theorem Matrix.mul_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (M : Matrix m n α) : M * 0 = 0

@[simp]

theorem Matrix.zero_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix m n α) : 0 * M = 0

theorem Matrix.mul_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (L : Matrix m n α) (M : Matrix n o α) (N : Matrix n o α) : L * (M + N) = L * M + L * N

theorem Matrix.add_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (L : Matrix l m α) (M : Matrix l m α) (N : Matrix m n α) : (L + M) * N = L * N + M * N

instance Matrix.nonUnitalNonAssocSemiring {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] : NonUnitalNonAssocSemiring (Matrix n n α)

Equations

• Matrix.nonUnitalNonAssocSemiring = let __src := Matrix.addCommMonoid; NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Matrix.diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (d : m → α) (M : Matrix m n α) (i : m) (j : n) : (Matrix.diagonal d * M) i j = d i * M i j

@[simp]

theorem Matrix.mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (d : n → α) (M : Matrix m n α) (i : m) (j : n) : (M * Matrix.diagonal d) i j = M i j * d j

@[simp]

theorem Matrix.diagonal_mul_diagonal {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (d₁ : n → α) (d₂ : n → α) : Matrix.diagonal d₁ * Matrix.diagonal d₂ = Matrix.diagonal fun (i : n) => d₁ i * d₂ i

theorem Matrix.diagonal_mul_diagonal' {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (d₁ : n → α) (d₂ : n → α) : Matrix.diagonal d₁ * Matrix.diagonal d₂ = Matrix.diagonal fun (i : n) => d₁ i * d₂ i

theorem Matrix.smul_eq_diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (M : Matrix m n α) (a : α) : a • M = (Matrix.diagonal fun (x : m) => a) * M

theorem Matrix.op_smul_eq_mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) : MulOpposite.op a • M = M * Matrix.diagonal fun (x : n) => a

@[simp]

theorem Matrix.addMonoidHomMulLeft_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix l m α) (x : Matrix m n α) : M.addMonoidHomMulLeft x = M * x

def Matrix.addMonoidHomMulLeft {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix l m α) : Matrix m n α →+ Matrix l n α

Left multiplication by a matrix, as an AddMonoidHom from matrices to matrices.

Equations

• M.addMonoidHomMulLeft = { toFun := fun (x : Matrix m n α) => M * x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.addMonoidHomMulRight_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix m n α) (x : Matrix l m α) : M.addMonoidHomMulRight x = x * M

def Matrix.addMonoidHomMulRight {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix m n α) : Matrix l m α →+ Matrix l n α

Right multiplication by a matrix, as an AddMonoidHom from matrices to matrices.

Equations

• M.addMonoidHomMulRight = { toFun := fun (x : Matrix l m α) => x * M, map_zero' := ⋯, map_add' := ⋯ }

theorem Matrix.sum_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [NonUnitalNonAssocSemiring α] [Fintype m] (s : Finset β) (f : β → Matrix l m α) (M : Matrix m n α) : (∑ a ∈ s, f a) * M = ∑ a ∈ s, f a * M

theorem Matrix.mul_sum {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [NonUnitalNonAssocSemiring α] [Fintype m] (s : Finset β) (f : β → Matrix m n α) (M : Matrix l m α) : M * ∑ a ∈ s, f a = ∑ a ∈ s, M * f a

instance Matrix.Semiring.isScalarTower {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] : IsScalarTower R (Matrix n n α) (Matrix n n α)

This instance enables use with smul_mul_assoc.

Equations

• ⋯ = ⋯

instance Matrix.Semiring.smulCommClass {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α] : SMulCommClass R (Matrix n n α) (Matrix n n α)

This instance enables use with mul_smul_comm.

Equations

• ⋯ = ⋯

@[simp]

theorem Matrix.one_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (M : Matrix m n α) : 1 * M = M

@[simp]

theorem Matrix.mul_one {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] [DecidableEq n] (M : Matrix m n α) : M * 1 = M

instance Matrix.nonAssocSemiring {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] [DecidableEq n] : NonAssocSemiring (Matrix n n α)

Equations

• Matrix.nonAssocSemiring = let __src := Matrix.nonUnitalNonAssocSemiring; let __src_1 := Matrix.instAddCommMonoidWithOne; NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Matrix.map_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [NonAssocSemiring α] [Fintype n] {L : Matrix m n α} {M : Matrix n o α} [NonAssocSemiring β] {f : α →+* β} : (L * M).map ⇑f = L.map ⇑f * M.map ⇑f

theorem Matrix.smul_one_eq_diagonal {m : Type u_2} {α : Type v} [NonAssocSemiring α] [DecidableEq m] (a : α) : a • 1 = Matrix.diagonal fun (x : m) => a

theorem Matrix.op_smul_one_eq_diagonal {m : Type u_2} {α : Type v} [NonAssocSemiring α] [DecidableEq m] (a : α) : MulOpposite.op a • 1 = Matrix.diagonal fun (x : m) => a

@[simp]

theorem Matrix.diagonalRingHom_apply (n : Type u_3) (α : Type v) [NonAssocSemiring α] [Fintype n] [DecidableEq n] (d : n → α) : (Matrix.diagonalRingHom n α) d = Matrix.diagonal d

def Matrix.diagonalRingHom (n : Type u_3) (α : Type v) [NonAssocSemiring α] [Fintype n] [DecidableEq n] : (n → α) →+* Matrix n n α

Matrix.diagonal as a RingHom.

Equations

• Matrix.diagonalRingHom n α = let __src := Matrix.diagonalAddMonoidHom n α; { toFun := Matrix.diagonal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem Matrix.mul_assoc {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype m] [Fintype n] (L : Matrix l m α) (M : Matrix m n α) (N : Matrix n o α) : L * M * N = L * (M * N)

instance Matrix.nonUnitalSemiring {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] : NonUnitalSemiring (Matrix n n α)

Equations

• Matrix.nonUnitalSemiring = let __src := Matrix.nonUnitalNonAssocSemiring; NonUnitalSemiring.mk ⋯

instance Matrix.semiring {n : Type u_3} {α : Type v} [Semiring α] [Fintype n] [DecidableEq n] : Semiring (Matrix n n α)

Equations

• Matrix.semiring = let __src := Matrix.nonUnitalSemiring; let __src_1 := Matrix.nonAssocSemiring; Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRec ⋯ ⋯

@[simp]

theorem Matrix.neg_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) : -M * N = -(M * N)

@[simp]

theorem Matrix.mul_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) : M * -N = -(M * N)

theorem Matrix.sub_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M : Matrix m n α) (M' : Matrix m n α) (N : Matrix n o α) : (M - M') * N = M * N - M' * N

theorem Matrix.mul_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) (N' : Matrix n o α) : M * (N - N') = M * N - M * N'

instance Matrix.nonUnitalNonAssocRing {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] : NonUnitalNonAssocRing (Matrix n n α)

Equations

• Matrix.nonUnitalNonAssocRing = let __src := Matrix.nonUnitalNonAssocSemiring; let __src_1 := Matrix.addCommGroup; NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

instance Matrix.instNonUnitalRing {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalRing α] : NonUnitalRing (Matrix n n α)

Equations

• Matrix.instNonUnitalRing = let __src := Matrix.nonUnitalSemiring; let __src_1 := Matrix.addCommGroup; NonUnitalRing.mk ⋯

instance Matrix.instNonAssocRing {n : Type u_3} {α : Type v} [Fintype n] [DecidableEq n] [NonAssocRing α] : NonAssocRing (Matrix n n α)

Equations

• Matrix.instNonAssocRing = let __src := Matrix.nonAssocSemiring; let __src_1 := Matrix.instAddCommGroupWithOne; NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Matrix.instRing {n : Type u_3} {α : Type v} [Fintype n] [DecidableEq n] [Ring α] : Ring (Matrix n n α)

Equations

• Matrix.instRing = let __src := Matrix.semiring; let __src_1 := Matrix.instAddCommGroupWithOne; Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem Matrix.diagonal_pow {n : Type u_3} {α : Type v} [Semiring α] [Fintype n] [DecidableEq n] (v : n → α) (k : ℕ) : Matrix.diagonal v ^ k = Matrix.diagonal (v ^ k)

@[simp]

theorem Matrix.mul_mul_left {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Semiring α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) : (Matrix.of fun (i : m) (j : n) => a * M i j) * N = a • (M * N)

def Matrix.scalar {α : Type v} [Semiring α] (n : Type u) [DecidableEq n] [Fintype n] : α →+* Matrix n n α

The ring homomorphism α →+* Matrix n n α sending a to the diagonal matrix with a on the diagonal.

Equations

• Matrix.scalar n = (Matrix.diagonalRingHom n α).comp (Pi.constRingHom n α)

@[simp]

theorem Matrix.scalar_apply {n : Type u_3} {α : Type v} [Semiring α] [DecidableEq n] [Fintype n] (a : α) : (Matrix.scalar n) a = Matrix.diagonal fun (x : n) => a

theorem Matrix.scalar_inj {n : Type u_3} {α : Type v} [Semiring α] [DecidableEq n] [Fintype n] [Nonempty n] {r : α} {s : α} : (Matrix.scalar n) r = (Matrix.scalar n) s ↔ r = s

theorem Matrix.scalar_commute_iff {n : Type u_3} {α : Type v} [Semiring α] [DecidableEq n] [Fintype n] {r : α} {M : Matrix n n α} : Commute ((Matrix.scalar n) r) M ↔ r • M = MulOpposite.op r • M

theorem Matrix.scalar_commute {n : Type u_3} {α : Type v} [Semiring α] [DecidableEq n] [Fintype n] (r : α) (hr : ∀ (r' : α), Commute r r') (M : Matrix n n α) : Commute ((Matrix.scalar n) r) M

theorem Matrix.smul_eq_mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [CommSemiring α] [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) : a • M = M * Matrix.diagonal fun (x : n) => a

@[simp]

theorem Matrix.mul_mul_right {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [CommSemiring α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) : (M * Matrix.of fun (i : n) (j : o) => a * N i j) = a • (M * N)

instance Matrix.instAlgebra {n : Type u_3} {R : Type u_7} {α : Type v} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] : Algebra R (Matrix n n α)

Equations

• Matrix.instAlgebra = Algebra.mk ((Matrix.scalar n).comp (algebraMap R α)) ⋯ ⋯

theorem Matrix.algebraMap_matrix_apply {n : Type u_3} {R : Type u_7} {α : Type v} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] {r : R} {i : n} {j : n} : (algebraMap R (Matrix n n α)) r i j = if i = j then (algebraMap R α) r else 0

theorem Matrix.algebraMap_eq_diagonal {n : Type u_3} {R : Type u_7} {α : Type v} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] (r : R) : (algebraMap R (Matrix n n α)) r = Matrix.diagonal ((algebraMap R (n → α)) r)

theorem Matrix.algebraMap_eq_diagonalRingHom {n : Type u_3} {R : Type u_7} {α : Type v} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] : algebraMap R (Matrix n n α) = (Matrix.diagonalRingHom n α).comp (algebraMap R (n → α))

@[simp]

theorem Matrix.map_algebraMap {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (r : R) (f : α → β) (hf : f 0 = 0) (hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r) : ((algebraMap R (Matrix n n α)) r).map f = (algebraMap R (Matrix n n β)) r

@[simp]

theorem Matrix.diagonalAlgHom_apply {n : Type u_3} (R : Type u_7) {α : Type v} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] (d : n → α) : (Matrix.diagonalAlgHom R) d = Matrix.diagonal d

def Matrix.diagonalAlgHom {n : Type u_3} (R : Type u_7) {α : Type v} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] : (n → α) →ₐ[R] Matrix n n α

Matrix.diagonal as an AlgHom.

Equations

• Matrix.diagonalAlgHom R = let __src := Matrix.diagonalRingHom n α; { toFun := Matrix.diagonal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Bundled versions of Matrix.map

@[simp]

theorem Equiv.mapMatrix_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α ≃ β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f

def Equiv.mapMatrix {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α ≃ β) : Matrix m n α ≃ Matrix m n β

The Equiv between spaces of matrices induced by an Equiv between their coefficients. This is Matrix.map as an Equiv.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m n α) => M.map ⇑f, invFun := fun (M : Matrix m n β) => M.map ⇑f.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.mapMatrix_refl {m : Type u_2} {n : Type u_3} {α : Type v} : (Equiv.refl α).mapMatrix = Equiv.refl (Matrix m n α)

@[simp]

theorem Equiv.mapMatrix_symm {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α ≃ β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem Equiv.mapMatrix_trans {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} (f : α ≃ β) (g : β ≃ γ) : f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix

@[simp]

theorem AddMonoidHom.mapMatrix_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f

def AddMonoidHom.mapMatrix {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) : Matrix m n α →+ Matrix m n β

The AddMonoidHom between spaces of matrices induced by an AddMonoidHom between their coefficients. This is Matrix.map as an AddMonoidHom.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m n α) => M.map ⇑f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.mapMatrix_id {m : Type u_2} {n : Type u_3} {α : Type v} [AddZeroClass α] : (AddMonoidHom.id α).mapMatrix = AddMonoidHom.id (Matrix m n α)

@[simp]

theorem AddMonoidHom.mapMatrix_comp {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+ γ) (g : α →+ β) : f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix

@[simp]

theorem AddEquiv.mapMatrix_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Add α] [Add β] (f : α ≃+ β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f

def AddEquiv.mapMatrix {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Add α] [Add β] (f : α ≃+ β) : Matrix m n α ≃+ Matrix m n β

The AddEquiv between spaces of matrices induced by an AddEquiv between their coefficients. This is Matrix.map as an AddEquiv.

Equations

• f.mapMatrix = let __src := f.mapMatrix; { toFun := fun (M : Matrix m n α) => M.map ⇑f, invFun := fun (M : Matrix m n β) => M.map ⇑f.symm, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem AddEquiv.mapMatrix_refl {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] : (AddEquiv.refl α).mapMatrix = AddEquiv.refl (Matrix m n α)

@[simp]

theorem AddEquiv.mapMatrix_symm {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Add α] [Add β] (f : α ≃+ β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem AddEquiv.mapMatrix_trans {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} [Add α] [Add β] [Add γ] (f : α ≃+ β) (g : β ≃+ γ) : f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix

@[simp]

theorem LinearMap.mapMatrix_apply {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α →ₗ[R] β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f

def LinearMap.mapMatrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α →ₗ[R] β) : Matrix m n α →ₗ[R] Matrix m n β

The LinearMap between spaces of matrices induced by a LinearMap between their coefficients. This is Matrix.map as a LinearMap.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m n α) => M.map ⇑f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.mapMatrix_id {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Semiring R] [AddCommMonoid α] [Module R α] : LinearMap.id.mapMatrix = LinearMap.id

@[simp]

theorem LinearMap.mapMatrix_comp {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} {γ : Type u_9} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (f : β →ₗ[R] γ) (g : α →ₗ[R] β) : f.mapMatrix ∘ₗ g.mapMatrix = (f ∘ₗ g).mapMatrix

@[simp]

theorem LinearEquiv.mapMatrix_apply {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α ≃ₗ[R] β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f

def LinearEquiv.mapMatrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α ≃ₗ[R] β) : Matrix m n α ≃ₗ[R] Matrix m n β

The LinearEquiv between spaces of matrices induced by a LinearEquiv between their coefficients. This is Matrix.map as a LinearEquiv.

Equations

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

@[simp]

theorem LinearEquiv.mapMatrix_refl {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Semiring R] [AddCommMonoid α] [Module R α] : (LinearEquiv.refl R α).mapMatrix = LinearEquiv.refl R (Matrix m n α)

@[simp]

theorem LinearEquiv.mapMatrix_symm {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α ≃ₗ[R] β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem LinearEquiv.mapMatrix_trans {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} {γ : Type u_9} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (f : α ≃ₗ[R] β) (g : β ≃ₗ[R] γ) : f.mapMatrix ≪≫ₗ g.mapMatrix = (f ≪≫ₗ g).mapMatrix

@[simp]

theorem RingHom.mapMatrix_apply {m : Type u_2} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f

def RingHom.mapMatrix {m : Type u_2} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) : Matrix m m α →+* Matrix m m β

The RingHom between spaces of square matrices induced by a RingHom between their coefficients. This is Matrix.map as a RingHom.

Equations

• f.mapMatrix = let __src := f.toAddMonoidHom.mapMatrix; { toFun := fun (M : Matrix m m α) => M.map ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.mapMatrix_id {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonAssocSemiring α] : (RingHom.id α).mapMatrix = RingHom.id (Matrix m m α)

@[simp]

theorem RingHom.mapMatrix_comp {m : Type u_2} {α : Type v} {β : Type w} {γ : Type u_9} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] [NonAssocSemiring γ] (f : β →+* γ) (g : α →+* β) : f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix

@[simp]

theorem RingEquiv.mapMatrix_apply {m : Type u_2} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α ≃+* β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f

def RingEquiv.mapMatrix {m : Type u_2} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α ≃+* β) : Matrix m m α ≃+* Matrix m m β

The RingEquiv between spaces of square matrices induced by a RingEquiv between their coefficients. This is Matrix.map as a RingEquiv.

Equations

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

@[simp]

theorem RingEquiv.mapMatrix_refl {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonAssocSemiring α] : (RingEquiv.refl α).mapMatrix = RingEquiv.refl (Matrix m m α)

@[simp]

theorem RingEquiv.mapMatrix_symm {m : Type u_2} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α ≃+* β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem RingEquiv.mapMatrix_trans {m : Type u_2} {α : Type v} {β : Type w} {γ : Type u_9} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] [NonAssocSemiring γ] (f : α ≃+* β) (g : β ≃+* γ) : f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix

@[simp]

theorem AlgHom.mapMatrix_apply {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f

def AlgHom.mapMatrix {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) : Matrix m m α →ₐ[R] Matrix m m β

The AlgHom between spaces of square matrices induced by an AlgHom between their coefficients. This is Matrix.map as an AlgHom.

Equations

• f.mapMatrix = let __src := f.mapMatrix; { toFun := fun (M : Matrix m m α) => M.map ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgHom.mapMatrix_id {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Algebra R α] : (AlgHom.id R α).mapMatrix = AlgHom.id R (Matrix m m α)

@[simp]

theorem AlgHom.mapMatrix_comp {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} {γ : Type u_9} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Semiring γ] [Algebra R α] [Algebra R β] [Algebra R γ] (f : β →ₐ[R] γ) (g : α →ₐ[R] β) : f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix

@[simp]

theorem AlgEquiv.mapMatrix_apply {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α ≃ₐ[R] β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f

def AlgEquiv.mapMatrix {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α ≃ₐ[R] β) : Matrix m m α ≃ₐ[R] Matrix m m β

The AlgEquiv between spaces of square matrices induced by an AlgEquiv between their coefficients. This is Matrix.map as an AlgEquiv.

Equations

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

@[simp]

theorem AlgEquiv.mapMatrix_refl {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Algebra R α] : AlgEquiv.refl.mapMatrix = AlgEquiv.refl

@[simp]

theorem AlgEquiv.mapMatrix_symm {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α ≃ₐ[R] β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem AlgEquiv.mapMatrix_trans {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} {γ : Type u_9} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Semiring γ] [Algebra R α] [Algebra R β] [Algebra R γ] (f : α ≃ₐ[R] β) (g : β ≃ₐ[R] γ) : f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix

def Matrix.vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] (w : m → α) (v : n → α) : Matrix m n α

For two vectors w and v, vecMulVec w v i j is defined to be w i * v j. Put another way, vecMulVec w v is exactly col w * row v.

Equations

• Matrix.vecMulVec w v = Matrix.of fun (x : m) (y : n) => w x * v y

theorem Matrix.vecMulVec_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] (w : m → α) (v : n → α) (i : m) (j : n) : Matrix.vecMulVec w v i j = w i * v j

def Matrix.mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (M : Matrix m n α) (v : n → α) : m → α

M *ᵥ v (notation for mulVec M v) is the matrix-vector product of matrix M and vector v, where v is seen as a column vector. Put another way, M *ᵥ v is the vector whose entries are those of M * col v (see col_mulVec).

The notation has precedence 73, which comes immediately before ⬝ᵥ for Matrix.dotProduct, so that A *ᵥ v ⬝ᵥ B *ᵥ w is parsed as (A *ᵥ v) ⬝ᵥ (B *ᵥ w).

Equations

• M.mulVec v x = let i := x; Matrix.dotProduct (fun (j : n) => M i j) v

def Matrix.«term_*ᵥ_» : Lean.TrailingParserDescr

M *ᵥ v (notation for mulVec M v) is the matrix-vector product of matrix M and vector v, where v is seen as a column vector. Put another way, M *ᵥ v is the vector whose entries are those of M * col v (see col_mulVec).

The notation has precedence 73, which comes immediately before ⬝ᵥ for Matrix.dotProduct, so that A *ᵥ v ⬝ᵥ B *ᵥ w is parsed as (A *ᵥ v) ⬝ᵥ (B *ᵥ w).

Equations

• Matrix.«term_*ᵥ_» = Lean.ParserDescr.trailingNode `Matrix.term_*ᵥ_ 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *ᵥ ") (Lean.ParserDescr.cat `term 73))

def Matrix.vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (v : m → α) (M : Matrix m n α) : n → α

v ᵥ* M (notation for vecMul v M) is the vector-matrix product of vector v and matrix M, where v is seen as a row vector. Put another way, v ᵥ* M is the vector whose entries are those of row v * M (see row_vecMul).

The notation has precedence 73, which comes immediately before ⬝ᵥ for Matrix.dotProduct, so that v ᵥ* A ⬝ᵥ w ᵥ* B is parsed as (v ᵥ* A) ⬝ᵥ (w ᵥ* B).

Equations

• Matrix.vecMul v M x = let j := x; Matrix.dotProduct v fun (i : m) => M i j

def Matrix.«term_ᵥ*_» : Lean.TrailingParserDescr

v ᵥ* M (notation for vecMul v M) is the vector-matrix product of vector v and matrix M, where v is seen as a row vector. Put another way, v ᵥ* M is the vector whose entries are those of row v * M (see row_vecMul).

The notation has precedence 73, which comes immediately before ⬝ᵥ for Matrix.dotProduct, so that v ᵥ* A ⬝ᵥ w ᵥ* B is parsed as (v ᵥ* A) ⬝ᵥ (w ᵥ* B).

Equations

• Matrix.«term_ᵥ*_» = Lean.ParserDescr.trailingNode `Matrix.term_ᵥ*_ 73 73 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᵥ* ") (Lean.ParserDescr.cat `term 74))

@[simp]

theorem Matrix.mulVec.addMonoidHomLeft_apply {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : n → α) (M : Matrix m n α) : ∀ (a : m), (Matrix.mulVec.addMonoidHomLeft v) M a = M.mulVec v a

def Matrix.mulVec.addMonoidHomLeft {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : n → α) : Matrix m n α →+ m → α

Left multiplication by a matrix, as an AddMonoidHom from vectors to vectors.

Equations

• Matrix.mulVec.addMonoidHomLeft v = { toFun := fun (M : Matrix m n α) => M.mulVec v, map_zero' := ⋯, map_add' := ⋯ }

theorem Matrix.mul_apply_eq_vecMul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A : Matrix m n α) (B : Matrix n o α) (i : m) : (A * B) i = Matrix.vecMul (A i) B

The ith row of the multiplication is the same as the vecMul with the ith row of A.

theorem Matrix.mulVec_diagonal {m : Type u_2} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (v : m → α) (w : m → α) (x : m) : (Matrix.diagonal v).mulVec w x = v x * w x

theorem Matrix.vecMul_diagonal {m : Type u_2} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (v : m → α) (w : m → α) (x : m) : Matrix.vecMul v (Matrix.diagonal w) x = v x * w x

theorem Matrix.dotProduct_mulVec {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype n] [Fintype m] [NonUnitalSemiring R] (v : m → R) (A : Matrix m n R) (w : n → R) : Matrix.dotProduct v (A.mulVec w) = Matrix.dotProduct (Matrix.vecMul v A) w

Associate the dot product of mulVec to the left.

@[simp]

theorem Matrix.mulVec_zero {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A : Matrix m n α) : A.mulVec 0 = 0

@[simp]

theorem Matrix.zero_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (A : Matrix m n α) : Matrix.vecMul 0 A = 0

@[simp]

theorem Matrix.zero_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : n → α) : Matrix.mulVec 0 v = 0

@[simp]

theorem Matrix.vecMul_zero {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (v : m → α) : Matrix.vecMul v 0 = 0

theorem Matrix.smul_mulVec_assoc {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] (a : R) (A : Matrix m n α) (b : n → α) : (a • A).mulVec b = a • A.mulVec b

theorem Matrix.mulVec_add {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A : Matrix m n α) (x : n → α) (y : n → α) : A.mulVec (x + y) = A.mulVec x + A.mulVec y

theorem Matrix.add_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A : Matrix m n α) (B : Matrix m n α) (x : n → α) : (A + B).mulVec x = A.mulVec x + B.mulVec x

theorem Matrix.vecMul_add {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (A : Matrix m n α) (B : Matrix m n α) (x : m → α) : Matrix.vecMul x (A + B) = Matrix.vecMul x A + Matrix.vecMul x B

theorem Matrix.add_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (A : Matrix m n α) (x : m → α) (y : m → α) : Matrix.vecMul (x + y) A = Matrix.vecMul x A + Matrix.vecMul y A

theorem Matrix.vecMul_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [Monoid R] [NonUnitalNonAssocSemiring S] [DistribMulAction R S] [IsScalarTower R S S] (M : Matrix n m S) (b : R) (v : n → S) : Matrix.vecMul (b • v) M = b • Matrix.vecMul v M

theorem Matrix.mulVec_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [Monoid R] [NonUnitalNonAssocSemiring S] [DistribMulAction R S] [SMulCommClass R S S] (M : Matrix m n S) (b : R) (v : n → S) : M.mulVec (b • v) = b • M.mulVec v

@[simp]

theorem Matrix.mulVec_single {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (M : Matrix m n R) (j : n) (x : R) : M.mulVec (Pi.single j x) = fun (i : m) => M i j * x

@[simp]

theorem Matrix.single_vecMul {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring R] (M : Matrix m n R) (i : m) (x : R) : Matrix.vecMul (Pi.single i x) M = fun (j : n) => x * M i j

theorem Matrix.diagonal_mulVec_single {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R) (j : n) (x : R) : (Matrix.diagonal v).mulVec (Pi.single j x) = Pi.single j (v j * x)

theorem Matrix.single_vecMul_diagonal {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R) (j : n) (x : R) : Matrix.vecMul (Pi.single j x) (Matrix.diagonal v) = Pi.single j (x * v j)

@[simp]

theorem Matrix.vecMul_vecMul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype n] [Fintype m] (v : m → α) (M : Matrix m n α) (N : Matrix n o α) : Matrix.vecMul (Matrix.vecMul v M) N = Matrix.vecMul v (M * N)

@[simp]

theorem Matrix.mulVec_mulVec {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype n] [Fintype o] (v : o → α) (M : Matrix m n α) (N : Matrix n o α) : M.mulVec (N.mulVec v) = (M * N).mulVec v

theorem Matrix.star_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] [StarRing α] (M : Matrix m n α) (v : n → α) : star (M.mulVec v) = Matrix.vecMul (star v) M.conjTranspose

theorem Matrix.star_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] [StarRing α] (M : Matrix m n α) (v : m → α) : star (Matrix.vecMul v M) = M.conjTranspose.mulVec (star v)

theorem Matrix.mulVec_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] [StarRing α] (A : Matrix m n α) (x : m → α) : A.conjTranspose.mulVec x = star (Matrix.vecMul (star x) A)

theorem Matrix.vecMul_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] [StarRing α] (A : Matrix m n α) (x : n → α) : Matrix.vecMul x A.conjTranspose = star (A.mulVec (star x))

theorem Matrix.mul_mul_apply {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] (A : Matrix n n α) (B : Matrix n n α) (C : Matrix n n α) (i : n) (j : n) : (A * B * C) i j = Matrix.dotProduct (A i) (B.mulVec (C.transpose j))

theorem Matrix.mulVec_one {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] (A : Matrix m n α) : A.mulVec 1 = fun (i : m) => ∑ j : n, A i j

theorem Matrix.vec_one_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] (A : Matrix m n α) : Matrix.vecMul 1 A = fun (j : n) => ∑ i : m, A i j

@[simp]

theorem Matrix.one_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (v : m → α) : Matrix.mulVec 1 v = v

@[simp]

theorem Matrix.vecMul_one {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (v : m → α) : Matrix.vecMul v 1 = v

@[simp]

theorem Matrix.diagonal_const_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : α) (v : m → α) : (Matrix.diagonal fun (x_1 : m) => x).mulVec v = x • v

@[simp]

theorem Matrix.vecMul_diagonal_const {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : α) (v : m → α) : Matrix.vecMul v (Matrix.diagonal fun (x_1 : m) => x) = MulOpposite.op x • v

@[simp]

theorem Matrix.natCast_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ℕ) (v : m → α) : (↑x).mulVec v = ↑x • v

@[simp]

theorem Matrix.vecMul_natCast {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ℕ) (v : m → α) : Matrix.vecMul v ↑x = MulOpposite.op ↑x • v

@[simp]

theorem Matrix.ofNat_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ℕ) [x.AtLeastTwo] (v : m → α) : Matrix.mulVec (OfNat.ofNat x) v = OfNat.ofNat x • v

@[simp]

theorem Matrix.vecMul_ofNat {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ℕ) [x.AtLeastTwo] (v : m → α) : Matrix.vecMul v (OfNat.ofNat x) = MulOpposite.op (OfNat.ofNat x) • v

theorem Matrix.neg_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (v : m → α) (A : Matrix m n α) : Matrix.vecMul (-v) A = -Matrix.vecMul v A

theorem Matrix.vecMul_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (v : m → α) (A : Matrix m n α) : Matrix.vecMul v (-A) = -Matrix.vecMul v A

theorem Matrix.neg_vecMul_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (v : m → α) (A : Matrix m n α) : Matrix.vecMul (-v) (-A) = Matrix.vecMul v A

theorem Matrix.neg_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (v : n → α) (A : Matrix m n α) : (-A).mulVec v = -A.mulVec v

theorem Matrix.mulVec_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (v : n → α) (A : Matrix m n α) : A.mulVec (-v) = -A.mulVec v

theorem Matrix.neg_mulVec_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (v : n → α) (A : Matrix m n α) : (-A).mulVec (-v) = A.mulVec v

theorem Matrix.mulVec_sub {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (A : Matrix m n α) (x : n → α) (y : n → α) : A.mulVec (x - y) = A.mulVec x - A.mulVec y

theorem Matrix.sub_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (A : Matrix m n α) (B : Matrix m n α) (x : n → α) : (A - B).mulVec x = A.mulVec x - B.mulVec x

theorem Matrix.vecMul_sub {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (A : Matrix m n α) (B : Matrix m n α) (x : m → α) : Matrix.vecMul x (A - B) = Matrix.vecMul x A - Matrix.vecMul x B

theorem Matrix.sub_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (A : Matrix m n α) (x : m → α) (y : m → α) : Matrix.vecMul (x - y) A = Matrix.vecMul x A - Matrix.vecMul y A

theorem Matrix.mulVec_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalCommSemiring α] [Fintype m] (A : Matrix m n α) (x : m → α) : A.transpose.mulVec x = Matrix.vecMul x A

theorem Matrix.vecMul_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalCommSemiring α] [Fintype n] (A : Matrix m n α) (x : n → α) : Matrix.vecMul x A.transpose = A.mulVec x

theorem Matrix.mulVec_vecMul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalCommSemiring α] [Fintype n] [Fintype o] (A : Matrix m n α) (B : Matrix o n α) (x : o → α) : A.mulVec (Matrix.vecMul x B) = (A * B.transpose).mulVec x

theorem Matrix.vecMul_mulVec {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalCommSemiring α] [Fintype m] [Fintype n] (A : Matrix m n α) (B : Matrix m o α) (x : n → α) : Matrix.vecMul (A.mulVec x) B = Matrix.vecMul x (A.transpose * B)

theorem Matrix.mulVec_smul_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [CommSemiring α] [Fintype n] (A : Matrix m n α) (b : n → α) (a : α) : A.mulVec (a • b) = a • A.mulVec b

@[simp]

theorem Matrix.intCast_mulVec {m : Type u_2} {α : Type v} [NonAssocRing α] [Fintype m] [DecidableEq m] (x : ℤ) (v : m → α) : (↑x).mulVec v = ↑x • v

@[simp]

theorem Matrix.vecMul_intCast {m : Type u_2} {α : Type v} [NonAssocRing α] [Fintype m] [DecidableEq m] (x : ℤ) (v : m → α) : Matrix.vecMul v ↑x = MulOpposite.op ↑x • v

@[simp]

theorem Matrix.transpose_transpose {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) : M.transpose.transpose = M

theorem Matrix.transpose_injective {m : Type u_2} {n : Type u_3} {α : Type v} : Function.Injective Matrix.transpose

@[simp]

theorem Matrix.transpose_inj {m : Type u_2} {n : Type u_3} {α : Type v} {A : Matrix m n α} {B : Matrix m n α} : A.transpose = B.transpose ↔ A = B

@[simp]

theorem Matrix.transpose_eq_diagonal {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] {M : Matrix n n α} {v : n → α} : M.transpose = Matrix.diagonal v ↔ M = Matrix.diagonal v

@[simp]

theorem Matrix.transpose_zero {m : Type u_2} {n : Type u_3} {α : Type v} [Zero α] : Matrix.transpose 0 = 0

@[simp]

theorem Matrix.transpose_eq_zero {m : Type u_2} {n : Type u_3} {α : Type v} [Zero α] {M : Matrix m n α} : M.transpose = 0 ↔ M = 0

@[simp]

theorem Matrix.transpose_one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] : Matrix.transpose 1 = 1

@[simp]

theorem Matrix.transpose_eq_one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] {M : Matrix n n α} : M.transpose = 1 ↔ M = 1

@[simp]

theorem Matrix.transpose_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] (d : ℕ) : (↑d).transpose = ↑d

@[simp]

theorem Matrix.transpose_eq_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] {M : Matrix n n α} {d : ℕ} : M.transpose = ↑d ↔ M = ↑d

@[simp]

theorem Matrix.transpose_ofNat {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] (d : ℕ) [d.AtLeastTwo] : (OfNat.ofNat d).transpose = OfNat.ofNat d

@[simp]

theorem Matrix.transpose_eq_ofNat {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] : M.transpose = OfNat.ofNat d ↔ M = OfNat.ofNat d

@[simp]

theorem Matrix.transpose_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [AddGroupWithOne α] (d : ℤ) : (↑d).transpose = ↑d

@[simp]

theorem Matrix.transpose_eq_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [AddGroupWithOne α] {M : Matrix n n α} {d : ℤ} : M.transpose = ↑d ↔ M = ↑d

@[simp]

theorem Matrix.transpose_add {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] (M : Matrix m n α) (N : Matrix m n α) : (M + N).transpose = M.transpose + N.transpose

@[simp]

theorem Matrix.transpose_sub {m : Type u_2} {n : Type u_3} {α : Type v} [Sub α] (M : Matrix m n α) (N : Matrix m n α) : (M - N).transpose = M.transpose - N.transpose

@[simp]

theorem Matrix.transpose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommMonoid α] [CommSemigroup α] [Fintype n] (M : Matrix m n α) (N : Matrix n l α) : (M * N).transpose = N.transpose * M.transpose

@[simp]

theorem Matrix.transpose_smul {m : Type u_2} {n : Type u_3} {α : Type v} {R : Type u_10} [SMul R α] (c : R) (M : Matrix m n α) : (c • M).transpose = c • M.transpose

@[simp]

theorem Matrix.transpose_neg {m : Type u_2} {n : Type u_3} {α : Type v} [Neg α] (M : Matrix m n α) : (-M).transpose = -M.transpose

theorem Matrix.transpose_map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {M : Matrix m n α} : M.transpose.map f = (M.map f).transpose

@[simp]

theorem Matrix.transposeAddEquiv_apply (m : Type u_2) (n : Type u_3) (α : Type v) [Add α] (M : Matrix m n α) : (Matrix.transposeAddEquiv m n α) M = M.transpose

def Matrix.transposeAddEquiv (m : Type u_2) (n : Type u_3) (α : Type v) [Add α] : Matrix m n α ≃+ Matrix n m α

Matrix.transpose as an AddEquiv

Equations

• Matrix.transposeAddEquiv m n α = { toFun := Matrix.transpose, invFun := Matrix.transpose, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.transposeAddEquiv_symm (m : Type u_2) (n : Type u_3) (α : Type v) [Add α] : (Matrix.transposeAddEquiv m n α).symm = Matrix.transposeAddEquiv n m α

theorem Matrix.transpose_list_sum {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] (l : List (Matrix m n α)) : l.sum.transpose = (List.map Matrix.transpose l).sum

theorem Matrix.transpose_multiset_sum {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommMonoid α] (s : Multiset (Matrix m n α)) : s.sum.transpose = (Multiset.map Matrix.transpose s).sum

theorem Matrix.transpose_sum {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommMonoid α] {ι : Type u_10} (s : Finset ι) (M : ι → Matrix m n α) : (∑ i ∈ s, M i).transpose = ∑ i ∈ s, (M i).transpose

@[simp]

theorem Matrix.transposeLinearEquiv_apply (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [Semiring R] [AddCommMonoid α] [Module R α] : ∀ (a : Matrix m n α), (Matrix.transposeLinearEquiv m n R α) a = (Matrix.transposeAddEquiv m n α).toFun a

def Matrix.transposeLinearEquiv (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [Semiring R] [AddCommMonoid α] [Module R α] : Matrix m n α ≃ₗ[R] Matrix n m α

Matrix.transpose as a LinearMap

Equations

• Matrix.transposeLinearEquiv m n R α = let __src := Matrix.transposeAddEquiv m n α; { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Matrix.transposeLinearEquiv_symm (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [Semiring R] [AddCommMonoid α] [Module R α] : (Matrix.transposeLinearEquiv m n R α).symm = Matrix.transposeLinearEquiv n m R α

@[simp]

theorem Matrix.transposeRingEquiv_apply (m : Type u_2) (α : Type v) [AddCommMonoid α] [CommSemigroup α] [Fintype m] (M : Matrix m m α) : (Matrix.transposeRingEquiv m α) M = MulOpposite.op M.transpose

@[simp]

theorem Matrix.transposeRingEquiv_symm_apply (m : Type u_2) (α : Type v) [AddCommMonoid α] [CommSemigroup α] [Fintype m] (M : (Matrix m m α)ᵐᵒᵖ) : (Matrix.transposeRingEquiv m α).symm M = (MulOpposite.unop M).transpose

def Matrix.transposeRingEquiv (m : Type u_2) (α : Type v) [AddCommMonoid α] [CommSemigroup α] [Fintype m] : Matrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ

Matrix.transpose as a RingEquiv to the opposite ring

Equations

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

@[simp]

theorem Matrix.transpose_pow {m : Type u_2} {α : Type v} [CommSemiring α] [Fintype m] [DecidableEq m] (M : Matrix m m α) (k : ℕ) : (M ^ k).transpose = M.transpose ^ k

theorem Matrix.transpose_list_prod {m : Type u_2} {α : Type v} [CommSemiring α] [Fintype m] [DecidableEq m] (l : List (Matrix m m α)) : l.prod.transpose = (List.map Matrix.transpose l).reverse.prod

@[simp]

theorem Matrix.transposeAlgEquiv_apply (m : Type u_2) (R : Type u_7) (α : Type v) [CommSemiring R] [CommSemiring α] [Fintype m] [DecidableEq m] [Algebra R α] (M : Matrix m m α) : (Matrix.transposeAlgEquiv m R α) M = MulOpposite.op M.transpose

@[simp]

theorem Matrix.transposeAlgEquiv_symm_apply (m : Type u_2) (R : Type u_7) (α : Type v) [CommSemiring R] [CommSemiring α] [Fintype m] [DecidableEq m] [Algebra R α] : ∀ (a : (Matrix m m α)ᵐᵒᵖ), (Matrix.transposeAlgEquiv m R α).symm a = ((Matrix.transposeAddEquiv m m α).trans MulOpposite.opAddEquiv).invFun a

def Matrix.transposeAlgEquiv (m : Type u_2) (R : Type u_7) (α : Type v) [CommSemiring R] [CommSemiring α] [Fintype m] [DecidableEq m] [Algebra R α] : Matrix m m α ≃ₐ[R] (Matrix m m α)ᵐᵒᵖ

Matrix.transpose as an AlgEquiv to the opposite ring

Equations

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

@[simp]

theorem Matrix.conjTranspose_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Star α] (M : Matrix m n α) (i : m) (j : n) : M.conjTranspose j i = star (M i j)

Tell simp what the entries are in a conjugate transposed matrix.

Compare with mul_apply, diagonal_apply_eq, etc.

@[simp]

theorem Matrix.conjTranspose_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} [InvolutiveStar α] (M : Matrix m n α) : M.conjTranspose.conjTranspose = M

theorem Matrix.conjTranspose_injective {m : Type u_2} {n : Type u_3} {α : Type v} [InvolutiveStar α] : Function.Injective Matrix.conjTranspose

@[simp]

theorem Matrix.conjTranspose_inj {m : Type u_2} {n : Type u_3} {α : Type v} [InvolutiveStar α] {A : Matrix m n α} {B : Matrix m n α} : A.conjTranspose = B.conjTranspose ↔ A = B

@[simp]

theorem Matrix.conjTranspose_eq_diagonal {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoid α] [StarAddMonoid α] {M : Matrix n n α} {v : n → α} : M.conjTranspose = Matrix.diagonal v ↔ M = Matrix.diagonal (star v)

@[simp]

theorem Matrix.conjTranspose_zero {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] [StarAddMonoid α] : Matrix.conjTranspose 0 = 0

@[simp]

theorem Matrix.conjTranspose_eq_zero {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] [StarAddMonoid α] {M : Matrix m n α} : M.conjTranspose = 0 ↔ M = 0

@[simp]

theorem Matrix.conjTranspose_one {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] : Matrix.conjTranspose 1 = 1

@[simp]

theorem Matrix.conjTranspose_eq_one {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] {M : Matrix n n α} : M.conjTranspose = 1 ↔ M = 1

@[simp]

theorem Matrix.conjTranspose_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] (d : ℕ) : (↑d).conjTranspose = ↑d

@[simp]

theorem Matrix.conjTranspose_eq_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] {M : Matrix n n α} {d : ℕ} : M.conjTranspose = ↑d ↔ M = ↑d

@[simp]

theorem Matrix.conjTranspose_ofNat {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] (d : ℕ) [d.AtLeastTwo] : (OfNat.ofNat d).conjTranspose = OfNat.ofNat d

@[simp]

theorem Matrix.conjTranspose_eq_ofNat {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] : M.conjTranspose = OfNat.ofNat d ↔ M = OfNat.ofNat d

@[simp]

theorem Matrix.conjTranspose_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [Ring α] [StarRing α] (d : ℤ) : (↑d).conjTranspose = ↑d

@[simp]

theorem Matrix.conjTranspose_eq_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [Ring α] [StarRing α] {M : Matrix n n α} {d : ℤ} : M.conjTranspose = ↑d ↔ M = ↑d

@[simp]

theorem Matrix.conjTranspose_add {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] [StarAddMonoid α] (M : Matrix m n α) (N : Matrix m n α) : (M + N).conjTranspose = M.conjTranspose + N.conjTranspose

@[simp]

theorem Matrix.conjTranspose_sub {m : Type u_2} {n : Type u_3} {α : Type v} [AddGroup α] [StarAddMonoid α] (M : Matrix m n α) (N : Matrix m n α) : (M - N).conjTranspose = M.conjTranspose - N.conjTranspose

@[simp]

theorem Matrix.conjTranspose_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Star R] [Star α] [SMul R α] [StarModule R α] (c : R) (M : Matrix m n α) : (c • M).conjTranspose = star c • M.conjTranspose

Note that StarModule is quite a strong requirement; as such we also provide the following variants which this lemma would not apply to:

• Matrix.conjTranspose_smul_non_comm
• Matrix.conjTranspose_nsmul
• Matrix.conjTranspose_zsmul
• Matrix.conjTranspose_natCast_smul
• Matrix.conjTranspose_intCast_smul
• Matrix.conjTranspose_inv_natCast_smul
• Matrix.conjTranspose_inv_intCast_smul
• Matrix.conjTranspose_rat_smul
• Matrix.conjTranspose_ratCast_smul

@[simp]

theorem Matrix.conjTranspose_smul_non_comm {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Star R] [Star α] [SMul R α] [SMul Rᵐᵒᵖ α] (c : R) (M : Matrix m n α) (h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a) : (c • M).conjTranspose = MulOpposite.op (star c) • M.conjTranspose

theorem Matrix.conjTranspose_smul_self {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] [StarMul α] (c : α) (M : Matrix m n α) : (c • M).conjTranspose = MulOpposite.op (star c) • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_nsmul {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] [StarAddMonoid α] (c : ℕ) (M : Matrix m n α) : (c • M).conjTranspose = c • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_zsmul {m : Type u_2} {n : Type u_3} {α : Type v} [AddGroup α] [StarAddMonoid α] (c : ℤ) (M : Matrix m n α) : (c • M).conjTranspose = c • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_natCast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ) (M : Matrix m n α) : (↑c • M).conjTranspose = ↑c • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_ofNat_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ) [c.AtLeastTwo] (M : Matrix m n α) : (OfNat.ofNat c • M).conjTranspose = OfNat.ofNat c • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_intCast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Ring R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℤ) (M : Matrix m n α) : (↑c • M).conjTranspose = ↑c • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_inv_natCast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [DivisionSemiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ) (M : Matrix m n α) : ((↑c)⁻¹ • M).conjTranspose = (↑c)⁻¹ • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_inv_ofNat_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [DivisionSemiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ) [c.AtLeastTwo] (M : Matrix m n α) : ((OfNat.ofNat c)⁻¹ • M).conjTranspose = (OfNat.ofNat c)⁻¹ • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_inv_intCast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [DivisionRing R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℤ) (M : Matrix m n α) : ((↑c)⁻¹ • M).conjTranspose = (↑c)⁻¹ • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_ratCast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [DivisionRing R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℚ) (M : Matrix m n α) : (↑c • M).conjTranspose = ↑c • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_rat_smul {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommGroup α] [StarAddMonoid α] [Module ℚ α] (c : ℚ) (M : Matrix m n α) : (c • M).conjTranspose = c • M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalSemiring α] [StarRing α] (M : Matrix m n α) (N : Matrix n l α) : (M * N).conjTranspose = N.conjTranspose * M.conjTranspose

@[simp]

theorem Matrix.conjTranspose_neg {m : Type u_2} {n : Type u_3} {α : Type v} [AddGroup α] [StarAddMonoid α] (M : Matrix m n α) : (-M).conjTranspose = -M.conjTranspose

theorem Matrix.conjTranspose_map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Star α] [Star β] {A : Matrix m n α} (f : α → β) (hf : Function.Semiconj f star star) : A.conjTranspose.map f = (A.map f).conjTranspose

@[simp]

theorem Matrix.conjTranspose_eq_transpose_of_trivial {m : Type u_2} {n : Type u_3} {α : Type v} [Star α] [TrivialStar α] (A : Matrix m n α) : A.conjTranspose = A.transpose

When star x = x on the coefficients (such as the real numbers) conjTranspose and transpose are the same operation.

@[simp]

theorem Matrix.conjTransposeAddEquiv_apply (m : Type u_2) (n : Type u_3) (α : Type v) [AddMonoid α] [StarAddMonoid α] (M : Matrix m n α) : (Matrix.conjTransposeAddEquiv m n α) M = M.conjTranspose

def Matrix.conjTransposeAddEquiv (m : Type u_2) (n : Type u_3) (α : Type v) [AddMonoid α] [StarAddMonoid α] : Matrix m n α ≃+ Matrix n m α

Matrix.conjTranspose as an AddEquiv

Equations

• Matrix.conjTransposeAddEquiv m n α = { toFun := Matrix.conjTranspose, invFun := Matrix.conjTranspose, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.conjTransposeAddEquiv_symm (m : Type u_2) (n : Type u_3) (α : Type v) [AddMonoid α] [StarAddMonoid α] : (Matrix.conjTransposeAddEquiv m n α).symm = Matrix.conjTransposeAddEquiv n m α

theorem Matrix.conjTranspose_list_sum {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] [StarAddMonoid α] (l : List (Matrix m n α)) : l.sum.conjTranspose = (List.map Matrix.conjTranspose l).sum

theorem Matrix.conjTranspose_multiset_sum {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommMonoid α] [StarAddMonoid α] (s : Multiset (Matrix m n α)) : s.sum.conjTranspose = (Multiset.map Matrix.conjTranspose s).sum

theorem Matrix.conjTranspose_sum {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommMonoid α] [StarAddMonoid α] {ι : Type u_10} (s : Finset ι) (M : ι → Matrix m n α) : (∑ i ∈ s, M i).conjTranspose = ∑ i ∈ s, (M i).conjTranspose

@[simp]

theorem Matrix.conjTransposeLinearEquiv_apply (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [CommSemiring R] [StarRing R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] [StarModule R α] : ∀ (a : Matrix m n α), (Matrix.conjTransposeLinearEquiv m n R α) a = (Matrix.conjTransposeAddEquiv m n α).toFun a

def Matrix.conjTransposeLinearEquiv (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [CommSemiring R] [StarRing R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] [StarModule R α] : Matrix m n α ≃ₗ⋆[R] Matrix n m α

Matrix.conjTranspose as a LinearMap

Equations

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

@[simp]

theorem Matrix.conjTransposeLinearEquiv_symm (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [CommSemiring R] [StarRing R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] [StarModule R α] : (Matrix.conjTransposeLinearEquiv m n R α).symm = Matrix.conjTransposeLinearEquiv n m R α

@[simp]

theorem Matrix.conjTransposeRingEquiv_apply (m : Type u_2) (α : Type v) [Semiring α] [StarRing α] [Fintype m] (M : Matrix m m α) : (Matrix.conjTransposeRingEquiv m α) M = MulOpposite.op M.conjTranspose

@[simp]

theorem Matrix.conjTransposeRingEquiv_symm_apply (m : Type u_2) (α : Type v) [Semiring α] [StarRing α] [Fintype m] (M : (Matrix m m α)ᵐᵒᵖ) : (Matrix.conjTransposeRingEquiv m α).symm M = (MulOpposite.unop M).conjTranspose

def Matrix.conjTransposeRingEquiv (m : Type u_2) (α : Type v) [Semiring α] [StarRing α] [Fintype m] : Matrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ

Matrix.conjTranspose as a RingEquiv to the opposite ring

Equations

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

@[simp]

theorem Matrix.conjTranspose_pow {m : Type u_2} {α : Type v} [Semiring α] [StarRing α] [Fintype m] [DecidableEq m] (M : Matrix m m α) (k : ℕ) : (M ^ k).conjTranspose = M.conjTranspose ^ k

theorem Matrix.conjTranspose_list_prod {m : Type u_2} {α : Type v} [Semiring α] [StarRing α] [Fintype m] [DecidableEq m] (l : List (Matrix m m α)) : l.prod.conjTranspose = (List.map Matrix.conjTranspose l).reverse.prod

instance Matrix.instStar {n : Type u_3} {α : Type v} [Star α] : Star (Matrix n n α)

When α has a star operation, square matrices Matrix n n α have a star operation equal to Matrix.conjTranspose.

Equations

• Matrix.instStar = { star := Matrix.conjTranspose }

theorem Matrix.star_eq_conjTranspose {m : Type u_2} {α : Type v} [Star α] (M : Matrix m m α) : star M = M.conjTranspose

@[simp]

theorem Matrix.star_apply {n : Type u_3} {α : Type v} [Star α] (M : Matrix n n α) (i : n) (j : n) : star M i j = star (M j i)

instance Matrix.instInvolutiveStar {n : Type u_3} {α : Type v} [InvolutiveStar α] : InvolutiveStar (Matrix n n α)

Equations

• Matrix.instInvolutiveStar = InvolutiveStar.mk ⋯

instance Matrix.instStarAddMonoid {n : Type u_3} {α : Type v} [AddMonoid α] [StarAddMonoid α] : StarAddMonoid (Matrix n n α)

When α is a *-additive monoid, Matrix.star is also a *-additive monoid.

Equations

• Matrix.instStarAddMonoid = StarAddMonoid.mk ⋯

instance Matrix.instStarModule {n : Type u_3} {α : Type v} {β : Type w} [Star α] [Star β] [SMul α β] [StarModule α β] : StarModule α (Matrix n n β)

Equations

• ⋯ = ⋯

instance Matrix.instStarRing {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalSemiring α] [StarRing α] : StarRing (Matrix n n α)

When α is a *-(semi)ring, Matrix.star is also a *-(semi)ring.

Equations

• Matrix.instStarRing = StarRing.mk ⋯

theorem Matrix.star_mul {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalSemiring α] [StarRing α] (M : Matrix n n α) (N : Matrix n n α) : star (M * N) = star N * star M

A version of star_mul for * instead of *.

def Matrix.submatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) : Matrix l o α

Given maps (r_reindex : l → m) and (c_reindex : o → n) reindexing the rows and columns of a matrix M : Matrix m n α, the matrix M.submatrix r_reindex c_reindex : Matrix l o α is defined by (M.submatrix r_reindex c_reindex) i j = M (r_reindex i) (c_reindex j) for (i,j) : l × o. Note that the total number of row and columns does not have to be preserved.

Equations

• A.submatrix r_reindex c_reindex = Matrix.of fun (i : l) (j : o) => A (r_reindex i) (c_reindex j)

@[simp]

theorem Matrix.submatrix_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) (i : l) (j : o) : A.submatrix r_reindex c_reindex i j = A (r_reindex i) (c_reindex j)

@[simp]

theorem Matrix.submatrix_id_id {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : A.submatrix id id = A

@[simp]

theorem Matrix.submatrix_submatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {l₂ : Type u_10} {o₂ : Type u_11} (A : Matrix m n α) (r₁ : l → m) (c₁ : o → n) (r₂ : l₂ → l) (c₂ : o₂ → o) : (A.submatrix r₁ c₁).submatrix r₂ c₂ = A.submatrix (r₁ ∘ r₂) (c₁ ∘ c₂)

@[simp]

theorem Matrix.transpose_submatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) : (A.submatrix r_reindex c_reindex).transpose = A.transpose.submatrix c_reindex r_reindex

@[simp]

theorem Matrix.conjTranspose_submatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Star α] (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) : (A.submatrix r_reindex c_reindex).conjTranspose = A.conjTranspose.submatrix c_reindex r_reindex

theorem Matrix.submatrix_add {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Add α] (A : Matrix m n α) (B : Matrix m n α) : (A + B).submatrix = A.submatrix + B.submatrix

theorem Matrix.submatrix_neg {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Neg α] (A : Matrix m n α) : (-A).submatrix = -A.submatrix

theorem Matrix.submatrix_sub {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Sub α] (A : Matrix m n α) (B : Matrix m n α) : (A - B).submatrix = A.submatrix - B.submatrix

@[simp]

theorem Matrix.submatrix_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Zero α] : Matrix.submatrix 0 = 0

theorem Matrix.submatrix_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {R : Type u_10} [SMul R α] (r : R) (A : Matrix m n α) : (r • A).submatrix = r • A.submatrix

theorem Matrix.submatrix_map {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} (f : α → β) (e₁ : l → m) (e₂ : o → n) (A : Matrix m n α) : (A.map f).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f

theorem Matrix.submatrix_diagonal {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l → m) (he : Function.Injective e) : (Matrix.diagonal d).submatrix e e = Matrix.diagonal (d ∘ e)

Given a (m × m) diagonal matrix defined by a map d : m → α, if the reindexing map e is injective, then the resulting matrix is again diagonal.

theorem Matrix.submatrix_one {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l → m) (he : Function.Injective e) : Matrix.submatrix 1 e e = 1

theorem Matrix.submatrix_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type u_10} {q : Type u_11} (M : Matrix m n α) (N : Matrix n p α) (e₁ : l → m) (e₂ : o → n) (e₃ : q → p) (he₂ : Function.Bijective e₂) : (M * N).submatrix e₁ e₃ = M.submatrix e₁ e₂ * N.submatrix e₂ e₃

theorem Matrix.diag_submatrix {l : Type u_1} {m : Type u_2} {α : Type v} (A : Matrix m m α) (e : l → m) : (A.submatrix e e).diag = A.diag ∘ e

simp lemmas for Matrix.submatrixs interaction with Matrix.diagonal, 1, and Matrix.mul for when the mappings are bundled.

@[simp]

theorem Matrix.submatrix_diagonal_embedding {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l ↪ m) : (Matrix.diagonal d).submatrix ⇑e ⇑e = Matrix.diagonal (d ∘ ⇑e)

@[simp]

theorem Matrix.submatrix_diagonal_equiv {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l ≃ m) : (Matrix.diagonal d).submatrix ⇑e ⇑e = Matrix.diagonal (d ∘ ⇑e)

@[simp]

theorem Matrix.submatrix_one_embedding {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l ↪ m) : Matrix.submatrix 1 ⇑e ⇑e = 1

@[simp]

theorem Matrix.submatrix_one_equiv {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l ≃ m) : Matrix.submatrix 1 ⇑e ⇑e = 1

@[simp]

theorem Matrix.submatrix_mul_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [AddCommMonoid α] [Mul α] {p : Type u_10} {q : Type u_11} (M : Matrix m n α) (N : Matrix n p α) (e₁ : l → m) (e₂ : o ≃ n) (e₃ : q → p) : M.submatrix e₁ ⇑e₂ * N.submatrix (⇑e₂) e₃ = (M * N).submatrix e₁ e₃

theorem Matrix.submatrix_mulVec_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : o → α) (e₁ : l → m) (e₂ : o ≃ n) : (M.submatrix e₁ ⇑e₂).mulVec v = M.mulVec (v ∘ ⇑e₂.symm) ∘ e₁

theorem Matrix.submatrix_vecMul_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : l → α) (e₁ : l ≃ m) (e₂ : o → n) : Matrix.vecMul v (M.submatrix (⇑e₁) e₂) = Matrix.vecMul (v ∘ ⇑e₁.symm) M ∘ e₂

theorem Matrix.mul_submatrix_one {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : n ≃ o) (e₂ : l → o) (M : Matrix m n α) : M * Matrix.submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)

theorem Matrix.one_submatrix_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype m] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : l → o) (e₂ : m ≃ o) (M : Matrix m n α) : Matrix.submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id

def Matrix.reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) : Matrix m n α ≃ Matrix l o α

The natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence.

Equations

• Matrix.reindex eₘ eₙ = { toFun := fun (M : Matrix m n α) => M.submatrix ⇑eₘ.symm ⇑eₙ.symm, invFun := fun (M : Matrix l o α) => M.submatrix ⇑eₘ ⇑eₙ, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Matrix.reindex_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) : (Matrix.reindex eₘ eₙ) M = M.submatrix ⇑eₘ.symm ⇑eₙ.symm

theorem Matrix.reindex_refl_refl {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : (Matrix.reindex (Equiv.refl m) (Equiv.refl n)) A = A

@[simp]

theorem Matrix.reindex_symm {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) : (Matrix.reindex eₘ eₙ).symm = Matrix.reindex eₘ.symm eₙ.symm

@[simp]

theorem Matrix.reindex_trans {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {l₂ : Type u_10} {o₂ : Type u_11} (eₘ : m ≃ l) (eₙ : n ≃ o) (eₘ₂ : l ≃ l₂) (eₙ₂ : o ≃ o₂) : (Matrix.reindex eₘ eₙ).trans (Matrix.reindex eₘ₂ eₙ₂) = Matrix.reindex (eₘ.trans eₘ₂) (eₙ.trans eₙ₂)

theorem Matrix.transpose_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) : ((Matrix.reindex eₘ eₙ) M).transpose = (Matrix.reindex eₙ eₘ) M.transpose

theorem Matrix.conjTranspose_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Star α] (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) : ((Matrix.reindex eₘ eₙ) M).conjTranspose = (Matrix.reindex eₙ eₘ) M.conjTranspose

theorem Matrix.submatrix_mul_transpose_submatrix {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [AddCommMonoid α] [Mul α] (e : m ≃ n) (M : Matrix m n α) : M.submatrix id ⇑e * M.transpose.submatrix (⇑e) id = M * M.transpose

@[reducible, inline]

abbrev Matrix.subLeft {α : Type v} {m : ℕ} {l : ℕ} {r : ℕ} (A : Matrix (Fin m) (Fin (l + r)) α) : Matrix (Fin m) (Fin l) α

The left n × l part of an n × (l+r) matrix.

Equations

• A.subLeft = A.submatrix id (Fin.castAdd r)

@[reducible, inline]

abbrev Matrix.subRight {α : Type v} {m : ℕ} {l : ℕ} {r : ℕ} (A : Matrix (Fin m) (Fin (l + r)) α) : Matrix (Fin m) (Fin r) α

The right n × r part of an n × (l+r) matrix.

Equations

• A.subRight = A.submatrix id (Fin.natAdd l)

@[reducible, inline]

abbrev Matrix.subUp {α : Type v} {d : ℕ} {u : ℕ} {n : ℕ} (A : Matrix (Fin (u + d)) (Fin n) α) : Matrix (Fin u) (Fin n) α

The top u × n part of a (u+d) × n matrix.

Equations

• A.subUp = A.submatrix (Fin.castAdd d) id

@[reducible, inline]

abbrev Matrix.subDown {α : Type v} {d : ℕ} {u : ℕ} {n : ℕ} (A : Matrix (Fin (u + d)) (Fin n) α) : Matrix (Fin d) (Fin n) α

The bottom d × n part of a (u+d) × n matrix.

Equations

• A.subDown = A.submatrix (Fin.natAdd u) id

@[reducible, inline]

abbrev Matrix.subUpRight {α : Type v} {d : ℕ} {u : ℕ} {l : ℕ} {r : ℕ} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin u) (Fin r) α

The top-right u × r part of a (u+d) × (l+r) matrix.

Equations

• A.subUpRight = A.subRight.subUp

@[reducible, inline]

abbrev Matrix.subDownRight {α : Type v} {d : ℕ} {u : ℕ} {l : ℕ} {r : ℕ} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin d) (Fin r) α

The bottom-right d × r part of a (u+d) × (l+r) matrix.

Equations

• A.subDownRight = A.subRight.subDown

@[reducible, inline]

abbrev Matrix.subUpLeft {α : Type v} {d : ℕ} {u : ℕ} {l : ℕ} {r : ℕ} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin u) (Fin l) α

The top-left u × l part of a (u+d) × (l+r) matrix.

Equations

• A.subUpLeft = A.subLeft.subUp

@[reducible, inline]

abbrev Matrix.subDownLeft {α : Type v} {d : ℕ} {u : ℕ} {l : ℕ} {r : ℕ} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin d) (Fin l) α

The bottom-left d × l part of a (u+d) × (l+r) matrix.

Equations

• A.subDownLeft = A.subLeft.subDown

theorem RingHom.map_matrix_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [Fintype n] [NonAssocSemiring α] [NonAssocSemiring β] (M : Matrix m n α) (N : Matrix n o α) (i : m) (j : o) (f : α →+* β) : f ((M * N) i j) = (M.map ⇑f * N.map ⇑f) i j

theorem RingHom.map_dotProduct {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (v : n → R) (w : n → R) : f (Matrix.dotProduct v w) = Matrix.dotProduct (⇑f ∘ v) (⇑f ∘ w)

theorem RingHom.map_vecMul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix n m R) (v : n → R) (i : m) : f (Matrix.vecMul v M i) = Matrix.vecMul (⇑f ∘ v) (M.map ⇑f) i

theorem RingHom.map_mulVec {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix m n R) (v : n → R) (i : m) : f (M.mulVec v i) = (M.map ⇑f).mulVec (⇑f ∘ v) i