ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommGroup M₃<VAR>AddCommGroup M₄<VAR>Module R M₃<VAR>Module R M₄<VAR>g : M₃ →ₗ[R] M₄<GOAL>g.graph = LinearMap.ker ((-g).coprod LinearMap.id)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M →ₗ[R] M₂<GOAL>f.graph = LinearMap.range (LinearMap.id.prod f)
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>i : n<GOAL>IsLinearMap α fun b => A.cramerMap b i
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>IsLinearMap α A.cramerMap
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i : n<GOAL>A.cramer b i = (A.updateColumn i b).det
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i : n<GOAL>A.transpose.cramer b i = (A.updateRow i b).det
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>i : n<GOAL>A.transpose.cramer (A i) = Pi.single i A.det
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i : n<VAR>h : ∀ (j : n), b j = A j i<GOAL>A.cramer b = Pi.single i A.det
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<GOAL>Matrix.cramer 1 = 1
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>r : α<VAR>A : Matrix n n α<GOAL>(r • A).cramer = r ^ (Fintype.card n - 1) • A.cramer
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>Subsingleton n<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i : n<GOAL>A.cramer b i = b i
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>Nontrivial n<GOAL>Matrix.cramer 0 = 0
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>β : Type u_1<VAR>s : Finset β<VAR>f : β → n → α<GOAL>∑ x ∈ s, A.cramer (f x) = A.cramer (∑ x ∈ s, f x)
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>β : Type u_1<VAR>s : Finset β<VAR>f : n → β → α<VAR>i : n<GOAL>∑ x ∈ s, A.cramer (fun j => f j x) i = A.cramer (fun j => ∑ x ∈ s, f j x) i
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>CommRing α<VAR>A : Matrix m m α<VAR>e : n ≃ m<VAR>b : n → α<GOAL>(A.submatrix ⇑e ⇑e).cramer b = A.cramer (b ∘ ⇑e.symm) ∘ ⇑e
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>CommRing α<VAR>e : m ≃ n<VAR>A : Matrix m m α<VAR>b : n → α<GOAL>((Matrix.reindex e e) A).cramer b = A.cramer (b ∘ ⇑e) ∘ ⇑e.symm
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A.adjugate = Matrix.of fun i => A.transpose.cramer (Pi.single i 1)
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>i j : n<GOAL>A.adjugate i j = (A.updateRow j (Pi.single i 1)).det
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A.adjugate.transpose = A.transpose.adjugate
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>CommRing α<VAR>e : n ≃ m<VAR>A : Matrix m m α<GOAL>(A.submatrix ⇑e ⇑e).adjugate = A.adjugate.submatrix ⇑e ⇑e
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>CommRing α<VAR>e : m ≃ n<VAR>A : Matrix m m α<GOAL>((Matrix.reindex e e) A).adjugate = (Matrix.reindex e e) A.adjugate
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<GOAL>A.cramer b = A.adjugate.mulVec b
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>i j k : n<GOAL>A i k * A.adjugate k j = A.transpose.cramer (Pi.single k (A i k)) j
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A * A.adjugate = A.det • 1
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A.adjugate * A = A.det • 1
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>r : α<VAR>A : Matrix n n α<GOAL>(r • A).adjugate = r ^ (Fintype.card n - 1) • A.adjugate
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<GOAL>A.mulVec (A.cramer b) = A.det • b
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>Subsingleton n<VAR>A : Matrix n n α<GOAL>A.adjugate = 1
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : Fintype.card n = 1<GOAL>A.adjugate = 1
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>Nontrivial n<GOAL>Matrix.adjugate 0 = 0
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<GOAL>Matrix.adjugate 1 = 1
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>v : n → α<GOAL>(Matrix.diagonal v).adjugate = Matrix.diagonal fun i => ∏ j ∈ Finset.univ.erase i, v j
<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>M : Matrix n n R<GOAL>f.mapMatrix M.adjugate = (f.mapMatrix M).adjugate
<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>M : Matrix n n A<GOAL>f.mapMatrix M.adjugate = (f.mapMatrix M).adjugate
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A.adjugate.det = A.det ^ (Fintype.card n - 1)
<VAR>α : Type w<VAR>CommRing α<VAR>A : Matrix (Fin 0) (Fin 0) α<GOAL>A.adjugate = 0
<VAR>α : Type w<VAR>CommRing α<VAR>A : Matrix (Fin 1) (Fin 1) α<GOAL>A.adjugate = 1
<VAR>α : Type w<VAR>CommRing α<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) α<VAR>i j : Fin n.succ<GOAL>A.adjugate i j = (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det
<VAR>α : Type w<VAR>CommRing α<VAR>A : Matrix (Fin 2) (Fin 2) α<GOAL>A.adjugate = !![A 1 1, -A 0 1; -A 1 0, A 0 0]
<VAR>α : Type w<VAR>CommRing α<VAR>a b c d : α<GOAL>!![a, b; c, d].adjugate = !![d, -b; -c, a]
<VAR>α : Type w<VAR>CommRing α<VAR>A : Matrix (Fin 3) (Fin 3) α<GOAL>A.adjugate = !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1; -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0; A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
<VAR>α : Type w<VAR>CommRing α<VAR>a b c d e f g h i : α<GOAL>!![a, b, c; d, e, f; g, h, i].adjugate = !![e * i - f * h, -(b * i) + c * h, b * f - c * e; -(d * i) + f * g, a * i - c * g, -(a * f) + c * d; d * h - e * g, -(a * h) + b * g, a * e - b * d]
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>i : n<GOAL>A.det = ∑ j : n, A i j * A.adjugate j i
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>j : n<GOAL>A.det = ∑ i : n, A i j * A.adjugate j i
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>StarRing α<VAR>A : Matrix n n α<GOAL>A.adjugate.conjTranspose = A.conjTranspose.adjugate
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>hA : IsLeftRegular A.det<GOAL>IsRegular A
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>hA : IsLeftRegular A.det<VAR>hB : IsLeftRegular B.det<GOAL>(A * B).adjugate = B.adjugate * A.adjugate
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A B : Matrix n n α<GOAL>(A * B).adjugate = B.adjugate * A.adjugate
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>k : ℕ<GOAL>(A ^ k).adjugate = A.adjugate ^ k
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : Fintype.card n ≠ 1<GOAL>A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
<VAR>n : Type v<VAR>α : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Nontrivial n<GOAL>A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>n : ℕ<GOAL>A⁻¹ ^ n = (A ^ n)⁻¹
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>m n : ℕ<VAR>ha : IsUnit A.det<VAR>h : n ≤ m<GOAL>A ^ (m - n) = A ^ m * (A ^ n)⁻¹
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>m n : ℕ<GOAL>A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>n : ℤ<GOAL>1 ^ n = 1
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>z : ℤ<GOAL>z ≠ 0 → 0 ^ z = 0
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>n : ℤ<GOAL>0 ^ n = if n = 0 then 1 else 0
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>n : ℤ<GOAL>A⁻¹ ^ n = (A ^ n)⁻¹
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<GOAL>A ^ (-1) = A⁻¹
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>n : ℕ<GOAL>A ^ (-↑n) = (A ^ n)⁻¹
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>h : IsUnit A.det<VAR>n : ℤ<GOAL>IsUnit (A ^ n).det
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>z : ℤ<GOAL>IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>h : IsUnit A.det<VAR>n : ℤ<GOAL>A ^ (-n) = (A ^ n)⁻¹
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>h : IsUnit A.det<VAR>n : ℤ<GOAL>A⁻¹ ^ n = A ^ (-n)
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>h : IsUnit A.det<VAR>n : ℤ<GOAL>A ^ (n + 1) = A ^ n * A
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>h : IsUnit A.det<VAR>n : ℤ<GOAL>A ^ (n - 1) = A ^ n * A⁻¹
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>ha : IsUnit A.det<VAR>m n : ℤ<GOAL>A ^ (m + n) = A ^ m * A ^ n
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>m n : ℤ<VAR>hm : m ≤ 0<VAR>hn : n ≤ 0<GOAL>A ^ (m + n) = A ^ m * A ^ n
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>m n : ℤ<VAR>hm : 0 ≤ m<VAR>hn : 0 ≤ n<GOAL>A ^ (m + n) = A ^ m * A ^ n
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>h : IsUnit A.det<VAR>i : ℤ<GOAL>A ^ (1 + i) = A * A ^ i
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A X Y : Matrix n' n' R<VAR>hx : IsUnit X.det<VAR>hy : IsUnit Y.det<VAR>h : SemiconjBy A X Y<VAR>m : ℤ<GOAL>SemiconjBy A (X ^ m) (Y ^ m)
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A B : Matrix n' n' R<VAR>h : Commute A B<VAR>m : ℤ<GOAL>Commute A (B ^ m)
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A B : Matrix n' n' R<VAR>h : Commute A B<VAR>m : ℤ<GOAL>Commute (A ^ m) B
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A B : Matrix n' n' R<VAR>h : Commute A B<VAR>m n : ℤ<GOAL>Commute (A ^ m) (B ^ n)
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>n : ℤ<GOAL>Commute (A ^ n) A
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>n : ℤ<GOAL>Commute A (A ^ n)
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>m n : ℤ<GOAL>Commute (A ^ m) (A ^ n)
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>n : ℤ<GOAL>n ≠ -1 → A ^ (n + 1) = A ^ n * A
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>h : IsUnit A.det<VAR>m n : ℤ<GOAL>A ^ (m * n) = (A ^ m) ^ n
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>h : IsUnit A.det<VAR>m n : ℤ<GOAL>A ^ (m * n) = (A ^ n) ^ m
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>u : (Matrix n' n' R)ˣ<VAR>n : ℤ<GOAL>↑(u ^ n) = ↑u ^ n
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>Nonempty n'<VAR>Nontrivial R<VAR>A : Matrix n' n' R<VAR>ha : IsUnit A.det<VAR>z : ℤ<GOAL>A ^ z ≠ 0
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>ha : IsUnit A.det<VAR>z1 z2 : ℤ<GOAL>A ^ (z1 - z2) = A ^ z1 / A ^ z2
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A B : Matrix n' n' R<VAR>h : Commute A B<VAR>i : ℤ<GOAL>(A * B) ^ i = A ^ i * B ^ i
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>n : ℤ<VAR>A : Matrix n' n' R<VAR>h : IsUnit A.det<GOAL>A ^ (-n) * A ^ n = 1
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>n : ℕ<GOAL>(1 / A) ^ n = 1 / A ^ n
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>n : ℤ<GOAL>(1 / A) ^ n = 1 / A ^ n
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>n : ℤ<GOAL>(A ^ n)ᵀ = Aᵀ ^ n
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>StarRing R<VAR>A : Matrix n' n' R<VAR>n : ℤ<GOAL>(A ^ n)ᴴ = Aᴴ ^ n
<VAR>n' : Type u_1<VAR>DecidableEq n'<VAR>Fintype n'<VAR>R : Type u_2<VAR>CommRing R<VAR>A : Matrix n' n' R<VAR>h : A.IsSymm<VAR>k : ℤ<GOAL>(A ^ k).IsSymm
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Semiring R<VAR>Fintype n<VAR>DecidableEq n<VAR>v : n → R<VAR>c : R<VAR>i : n<GOAL>Matrix.dotProduct v ((LinearMap.stdBasis R (fun x => R) i) c) = v i * c
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Semiring R<VAR>Fintype n<VAR>DecidableEq n<VAR>v : n → R<VAR>i : n<GOAL>Matrix.dotProduct v ((LinearMap.stdBasis R (fun x => R) i) 1) = v i
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Semiring R<VAR>Fintype n<VAR>v w : n → R<VAR>h : ∀ (u : n → R), Matrix.dotProduct v u = Matrix.dotProduct w u<GOAL>v = w
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Semiring R<VAR>Fintype n<VAR>v w : n → R<GOAL>(∀ (u : n → R), Matrix.dotProduct v u = Matrix.dotProduct w u) ↔ v = w
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Semiring R<VAR>Fintype n<VAR>v : n → R<VAR>h : ∀ (w : n → R), Matrix.dotProduct v w = 0<GOAL>v = 0
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Semiring R<VAR>Fintype n<VAR>v : n → R<GOAL>(∀ (w : n → R), Matrix.dotProduct v w = 0) ↔ v = 0
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>OrderedSemiring R<VAR>Fintype n<VAR>v w : n → R<VAR>hv : 0 ≤ v<VAR>hw : 0 ≤ w<GOAL>0 ≤ Matrix.dotProduct v w
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>OrderedSemiring R<VAR>Fintype n<VAR>u v w : n → R<VAR>huv : u ≤ v<VAR>hw : 0 ≤ w<GOAL>Matrix.dotProduct u w ≤ Matrix.dotProduct v w
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>OrderedSemiring R<VAR>Fintype n<VAR>u v w : n → R<VAR>huv : u ≤ v<VAR>hw : 0 ≤ w<GOAL>Matrix.dotProduct w u ≤ Matrix.dotProduct w v
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>LinearOrderedRing R<VAR>v : n → R<GOAL>Matrix.dotProduct v v = 0 ↔ v = 0
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>v : n → R<GOAL>Matrix.dotProduct (star v) v = 0 ↔ v = 0
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>v : n → R<GOAL>Matrix.dotProduct v (star v) = 0 ↔ v = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype m<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>A : Matrix m n R<GOAL>A.conjTranspose * A = 0 ↔ A = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>A : Matrix m n R<GOAL>A * A.conjTranspose = 0 ↔ A = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>A : Matrix m n R<VAR>B : Matrix n p R<GOAL>A.conjTranspose * A * B = 0 ↔ A * B = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>A : Matrix m n R<VAR>B : Matrix m p R<GOAL>A * A.conjTranspose * B = 0 ↔ A.conjTranspose * B = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>A : Matrix m n R<VAR>B : Matrix p m R<GOAL>B * (A * A.conjTranspose) = 0 ↔ B * A = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>A : Matrix m n R<VAR>B : Matrix p n R<GOAL>B * (A.conjTranspose * A) = 0 ↔ B * A.conjTranspose = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>A : Matrix m n R<VAR>v : n → R<GOAL>(A.conjTranspose * A).mulVec v = 0 ↔ A.mulVec v = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>A : Matrix m n R<VAR>v : m → R<GOAL>(A * A.conjTranspose).mulVec v = 0 ↔ A.conjTranspose.mulVec v = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>A : Matrix m n R<VAR>v : n → R<GOAL>Matrix.vecMul v (A.conjTranspose * A) = 0 ↔ Matrix.vecMul v A.conjTranspose = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NoZeroDivisors R<VAR>A : Matrix m n R<VAR>v : m → R<GOAL>Matrix.vecMul v (A * A.conjTranspose) = 0 ↔ Matrix.vecMul v A = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i : ι<VAR>j : ι'<GOAL>e.toMatrix v i j = (e.repr (v j)) i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>j : ι'<GOAL>(e.toMatrix v)ᵀ j = ⇑(e.repr (v j))
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : Basis ι R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>v : ι → M<GOAL>e.toMatrix v = (LinearMap.toMatrix e e) ((e.constr ℕ) v)
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>CommSemiring R<VAR>Finite ι<GOAL>(Pi.basisFun R ι).toMatrix = Matrix.transpose
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : Basis ι R M<VAR>DecidableEq ι<GOAL>e.toMatrix ⇑e = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>j : ι'<VAR>DecidableEq ι'<VAR>x : M<GOAL>e.toMatrix (Function.update v j x) = (e.toMatrix v).updateColumn j ⇑(e.repr x)
<VAR>ι : Type u_1<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>CommRing R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>DecidableEq ι<VAR>e : Basis ι R₂ M₂<VAR>w : ι → R₂ˣ<GOAL>e.toMatrix ⇑(e.unitsSMul w) = Matrix.diagonal (Units.val ∘ w)
<VAR>ι : Type u_1<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>CommRing R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>DecidableEq ι<VAR>e : Basis ι R₂ M₂<VAR>w : ι → R₂<VAR>hw : ∀ (i : ι), IsUnit (w i)<GOAL>e.toMatrix ⇑(e.isUnitSMul hw) = Matrix.diagonal w
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>G : Type u_9<VAR>Group G<VAR>DistribMulAction G M<VAR>SMulCommClass G R M<VAR>g : G<GOAL>(g • e).toMatrix v = e.toMatrix (g⁻¹ • v)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>j : ι'<VAR>Fintype ι<GOAL>∑ i : ι, e.toMatrix v i j • e i = v j
<VAR>ι : Type u_1<VAR>R₁ : Type u_9<VAR>S : Type u_10<VAR>CommRing R₁<VAR>Ring S<VAR>Algebra R₁ S<VAR>Fintype ι<VAR>DecidableEq ι<VAR>x : S<VAR>b : Basis ι R₁ S<VAR>w : ι → S<GOAL>b.toMatrix (x • w) = (Algebra.leftMulMatrix b) x * b.toMatrix w
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_5<VAR>CommSemiring R<VAR>S : Type u_9<VAR>Ring S<VAR>Algebra R S<VAR>Fintype ι<VAR>b : Basis ι R S<VAR>v : ι' → S<GOAL>⇑b ᵥ* (b.toMatrix v).map ⇑(algebraMap R S) = v
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : Basis ι R M<VAR>Finite ι<VAR>Fintype ι'<VAR>DecidableEq ι'<VAR>v : Basis ι' R M<GOAL>(Matrix.toLin v e) (e.toMatrix ⇑v) = LinearMap.id
<VAR>ι : Type u_1<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>CommRing R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>Fintype ι<VAR>DecidableEq ι<VAR>S : Type u_9<VAR>CommRing S<VAR>Nontrivial S<VAR>Algebra R₂ S<VAR>Module S M₂<VAR>IsScalarTower R₂ S M₂<VAR>NoZeroSMulDivisors R₂ S<VAR>b : Basis ι S M₂<VAR>v : ι → ↥(Submodule.span R₂ (Set.range ⇑b))<GOAL>(algebraMap R₂ S).mapMatrix ((Basis.restrictScalars R₂ b).toMatrix v) = b.toMatrix fun i => ↑(v i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Finite ι'<GOAL>(LinearMap.toMatrix b b') LinearMap.id = b'.toMatrix ⇑b
<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_9<VAR>AddCommMonoid N<VAR>Module R N<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>Fintype ι'<VAR>Finite κ<VAR>Fintype κ'<VAR>DecidableEq ι'<GOAL>c.toMatrix ⇑c' * (LinearMap.toMatrix b' c') f = (LinearMap.toMatrix b' c) f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>R : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_9<VAR>AddCommMonoid N<VAR>Module R N<VAR>Fintype ι'<VAR>Fintype κ<VAR>Finite ι<VAR>DecidableEq κ<VAR>b₁ : Basis ι R M<VAR>b₂ : Basis ι' R M<VAR>b₃ : Basis κ R N<VAR>A : Matrix ι' κ R<GOAL>b₁.toMatrix ⇑b₂ * A = (LinearMap.toMatrix b₃ b₁) ((Matrix.toLin b₃ b₂) A)