ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>S : Type u_5<VAR>S₂ : Type u_6<VAR>M : Type u_7<VAR>N : Type u_8<VAR>P : Type u_9<VAR>Semiring R<VAR>Semiring S<VAR>Semiring R₂<VAR>Semiring S₂<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>b₁ : Basis ι₁ R M<VAR>b₂ : Basis ι₂ S N<VAR>B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>x : M<VAR>y : N<GOAL>((b₁.repr x).sum fun i xi => (b₂.repr y).sum fun j yj => ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) = (B x) y
<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>Rₗ : Type u_10<VAR>Mₗ : Type u_11<VAR>Nₗ : Type u_12<VAR>Pₗ : Type u_13<VAR>CommSemiring Rₗ<VAR>AddCommMonoid Mₗ<VAR>AddCommMonoid Nₗ<VAR>AddCommMonoid Pₗ<VAR>Module Rₗ Mₗ<VAR>Module Rₗ Nₗ<VAR>Module Rₗ Pₗ<VAR>b₁' : Basis ι₁ Rₗ Mₗ<VAR>b₂' : Basis ι₂ Rₗ Nₗ<VAR>B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ<VAR>x : Mₗ<VAR>y : Nₗ<GOAL>((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • (B (b₁' i)) (b₂' j)) = (B x) y
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<GOAL>M.det = ∑ σ : Equiv.Perm n, Equiv.Perm.sign σ • ∏ i : n, M (σ i) i
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<GOAL>M.det = ∑ σ : Equiv.Perm n, ↑↑(Equiv.Perm.sign σ) * ∏ i : n, M (σ i) i
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>d : n → R<GOAL>(Matrix.diagonal d).det = ∏ i : n, d i
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<GOAL>Nonempty n → Matrix.det 0 = 0
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<GOAL>Matrix.det 1 = 1
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>IsEmpty n<VAR>A : Matrix n n R<GOAL>A.det = 1
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>IsEmpty n<GOAL>Matrix.det = Function.const (Matrix n n R) 1
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>h : Fintype.card n = 0<GOAL>A.det = 1
<VAR>R : Type v<VAR>CommRing R<VAR>n : Type u_3<VAR>Unique n<VAR>DecidableEq n<VAR>Fintype n<VAR>A : Matrix n n R<GOAL>A.det = A default default
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>Subsingleton n<VAR>A : Matrix n n R<VAR>k : n<GOAL>A.det = A k k
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>h : Fintype.card n = 1<VAR>k : n<GOAL>A.det = A k k
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M N : Matrix n n R<VAR>p : n → n<VAR>H : ¬Function.Bijective p<GOAL>∑ σ : Equiv.Perm n, ↑↑(Equiv.Perm.sign σ) * ∏ x : n, M (σ x) (p x) * N (p x) x = 0
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M N : Matrix n n R<GOAL>(M * N).det = M.det * N.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<GOAL>⇑Matrix.detMonoidHom = Matrix.det
<VAR>m : Type u_1<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>M N : Matrix m m R<GOAL>(M * N).det = (N * M).det
<VAR>m : Type u_1<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>M N P : Matrix m m R<GOAL>(M * (N * P)).det = (N * (M * P)).det
<VAR>m : Type u_1<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>M N P : Matrix m m R<GOAL>(M * N * P).det = (M * P * N).det
<VAR>m : Type u_1<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>M : (Matrix m m R)ˣ<VAR>N : Matrix m m R<GOAL>(↑M * N * ↑M⁻¹).det = N.det
<VAR>m : Type u_1<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>M : (Matrix m m R)ˣ<VAR>N : Matrix m m R<GOAL>(↑M⁻¹ * N * ↑M).det = N.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<GOAL>M.transpose.det = M.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>σ : Equiv.Perm n<VAR>M : Matrix n n R<GOAL>(M.submatrix (⇑σ) id).det = ↑↑(Equiv.Perm.sign σ) * M.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>σ : Equiv.Perm n<VAR>M : Matrix n n R<GOAL>(M.submatrix id ⇑σ).det = ↑↑(Equiv.Perm.sign σ) * M.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>e : n ≃ m<VAR>A : Matrix m m R<GOAL>(A.submatrix ⇑e ⇑e).det = A.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>e : m ≃ n<VAR>A : Matrix m m R<GOAL>((Matrix.reindex e e) A).det = A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>c : R<GOAL>(c • A).det = c ^ Fintype.card n * A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>α : Type u_3<VAR>Monoid α<VAR>DistribMulAction α R<VAR>IsScalarTower α R R<VAR>SMulCommClass α R R<VAR>c : α<VAR>A : Matrix n n R<GOAL>(c • A).det = c ^ Fintype.card n • A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<GOAL>(-A).det = (-1) ^ Fintype.card n * A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<GOAL>(-A).det = (-1) ^ Fintype.card n • A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>v : n → R<VAR>A : Matrix n n R<GOAL>(Matrix.of fun i j => v j * A i j).det = (∏ i : n, v i) * A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>v : n → R<VAR>A : Matrix n n R<GOAL>(Matrix.of fun i j => v i * A i j).det = (∏ i : n, v i) * A.det
<VAR>m : Type u_1<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>n : ℕ<GOAL>(M ^ n).det = M.det ^ n
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>S : Type w<VAR>CommRing S<VAR>f : R →+* S<VAR>M : Matrix n n R<GOAL>f M.det = (f.mapMatrix M).det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>S : Type w<VAR>CommRing S<VAR>f : R ≃+* S<VAR>M : Matrix n n R<GOAL>f M.det = (f.mapMatrix M).det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>S : Type w<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type z<VAR>CommRing T<VAR>Algebra R T<VAR>f : S →ₐ[R] T<VAR>M : Matrix n n S<GOAL>f M.det = (f.mapMatrix M).det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>S : Type w<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type z<VAR>CommRing T<VAR>Algebra R T<VAR>f : S ≃ₐ[R] T<VAR>M : Matrix n n S<GOAL>f M.det = (f.mapMatrix M).det
<VAR>m : Type u_1<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>StarRing R<VAR>M : Matrix m m R<GOAL>M.conjTranspose.det = star M.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>i : n<VAR>h : ∀ (j : n), A i j = 0<GOAL>A.det = 0
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>j : n<VAR>h : ∀ (i : n), A i j = 0<GOAL>A.det = 0
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>i j : n<VAR>i_ne_j : i ≠ j<VAR>hij : M i = M j<GOAL>M.det = 0
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>i j : n<VAR>i_ne_j : i ≠ j<VAR>hij : ∀ (k : n), M k i = M k j<GOAL>M.det = 0
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>i j : n<VAR>h : i ≠ j<GOAL>(M.updateRow j (M i)).det = 0
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>i j : n<VAR>h : i ≠ j<GOAL>(M.updateColumn j fun k => M k i).det = 0
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>u v : n → R<GOAL>(M.updateRow j (u + v)).det = (M.updateRow j u).det + (M.updateRow j v).det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>u v : n → R<GOAL>(M.updateColumn j (u + v)).det = (M.updateColumn j u).det + (M.updateColumn j v).det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>s : R<VAR>u : n → R<GOAL>(M.updateRow j (s • u)).det = s * (M.updateRow j u).det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>s : R<VAR>u : n → R<GOAL>(M.updateColumn j (s • u)).det = s * (M.updateColumn j u).det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>s : R<VAR>u : n → R<GOAL>((s • M).updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateRow j u).det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>s : R<VAR>u : n → R<GOAL>((s • M).updateColumn j u).det = s ^ (Fintype.card n - 1) * (M.updateColumn j u).det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>s : Finset n<VAR>hj : j ∉ s<VAR>c : n → R<VAR>a : R<GOAL>(M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>j : n<VAR>c : n → R<GOAL>(A.updateRow j (∑ k : n, c k • A k)).det = c j • A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>j : n<VAR>c : n → R<GOAL>(A.updateColumn j fun k => ∑ i : n, c i • A k i).det = c j • A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A B : Matrix n n R<VAR>C : Matrix n n R<VAR>hC : C.det = 1<VAR>hA : A = B * C<GOAL>A.det = B.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A B : Matrix n n R<VAR>C : Matrix n n R<VAR>hC : C.det = 1<VAR>hA : A = C * B<GOAL>A.det = B.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>i j : n<VAR>hij : i ≠ j<GOAL>(A.updateRow i (A i + A j)).det = A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>i j : n<VAR>hij : i ≠ j<GOAL>(A.updateColumn i fun k => A k i + A k j).det = A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>i j : n<VAR>hij : i ≠ j<VAR>c : R<GOAL>(A.updateRow i (A i + c • A j)).det = A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>i j : n<VAR>hij : i ≠ j<VAR>c : R<GOAL>(A.updateColumn i fun k => A k i + c • A k j).det = A.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A B : Matrix n n R<VAR>s : Finset n<VAR>c : n → R<GOAL>(∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A B : Matrix n n R<VAR>c : n → R<VAR>k : n<VAR>hk : c k = 0<VAR>A_eq : ∀ (i j : n), A i j = B i j + c i * B k j<GOAL>A.det = B.det
<VAR>R : Type v<VAR>CommRing R<VAR>n : ℕ<VAR>k : Fin (n + 1)<VAR>c : Fin n → R<VAR>_hc : ∀ (i : Fin n), k < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<GOAL>M.det = N.det
<VAR>R : Type v<VAR>CommRing R<VAR>n : ℕ<VAR>A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R<VAR>c : Fin n → R<VAR>A_zero : ∀ (j : Fin (n + 1)), A 0 j = B 0 j<VAR>A_succ : ∀ (i : Fin n) (j : Fin (n + 1)), A i.succ j = B i.succ j + c i * A i.castSucc j<GOAL>A.det = B.det
<VAR>R : Type v<VAR>CommRing R<VAR>n : ℕ<VAR>A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R<VAR>c : Fin n → R<VAR>A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0<VAR>A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc<GOAL>A.det = B.det
<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>o : Type u_3<VAR>Fintype o<VAR>DecidableEq o<VAR>M : o → Matrix n n R<GOAL>(Matrix.blockDiagonal M).det = ∏ k : o, (M k).det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix m m R<VAR>B : Matrix m n R<VAR>D : Matrix n n R<GOAL>(Matrix.fromBlocks A B 0 D).det = A.det * D.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix m m R<VAR>C : Matrix n m R<VAR>D : Matrix n n R<GOAL>(Matrix.fromBlocks A 0 C D).det = A.det * D.det
<VAR>R : Type v<VAR>CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<GOAL>A.det = ∑ i : Fin n.succ, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det
<VAR>R : Type v<VAR>CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<GOAL>A.det = ∑ j : Fin n.succ, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det
<VAR>R : Type v<VAR>CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<GOAL>A.det = ∑ j : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
<VAR>R : Type v<VAR>CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>j : Fin n.succ<GOAL>A.det = ∑ i : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix (Fin 0) (Fin 0) R<GOAL>A.det = 1
<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix (Fin 1) (Fin 1) R<GOAL>A.det = A 0 0
<VAR>R : Type v<VAR>CommRing R<VAR>a : R<GOAL>!![a].det = a
<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix (Fin 2) (Fin 2) R<GOAL>A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0
<VAR>R : Type v<VAR>CommRing R<VAR>a b c d : R<GOAL>!![a, b; c, d].det = a * d - b * c
<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix (Fin 3) (Fin 3) R<GOAL>A.det = A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 + A 0 2 * A 1 0 * A 2 1 - A 0 2 * A 1 1 * A 2 0
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : Module.End K V<VAR>q : Polynomial K<VAR>hq : q.degree = 1<GOAL>f.eigenspace (-q.coeff 0 / q.leadingCoeff) = LinearMap.ker ((Polynomial.aeval f) q)
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : Module.End K V<VAR>c : (Polynomial K)ˣ<GOAL>LinearMap.ker ((Polynomial.aeval f) ↑c) = ⊥
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : Module.End K V<VAR>p : Polynomial K<VAR>μ : K<VAR>x : V<VAR>h : f.HasEigenvector μ x<GOAL>((Polynomial.aeval f) p) x = Polynomial.eval μ p • x
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : Module.End K V<VAR>μ : K<VAR>h : f.HasEigenvalue μ<GOAL>(minpoly K f).IsRoot μ
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>μ : K<VAR>h : (minpoly K f).IsRoot μ<GOAL>f.HasEigenvalue μ
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>μ : K<GOAL>f.HasEigenvalue μ ↔ (minpoly K f).IsRoot μ
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<GOAL>Set.Finite f.HasEigenvalue
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<GOAL>(spectrum K f).Finite
<VAR>n : Type u_1<VAR>R : Type u_2<VAR>Field R<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n R<GOAL>(spectrum R A).Finite
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<GOAL>b.flag 0 = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<GOAL>b.flag (Fin.last n) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>k : Fin (n + 1)<VAR>p : Submodule R M<GOAL>b.flag k ≤ p ↔ ∀ (i : Fin n), i.castSucc < k → b i ∈ p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>k : Fin n<GOAL>b.flag k.succ = Submodule.span R {b k} ⊔ b.flag k.castSucc
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>i : Fin n<VAR>k : Fin (n + 1)<VAR>h : i.castSucc < k<GOAL>b i ∈ b.flag k
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>Nontrivial R<VAR>b : Basis (Fin n) R M<VAR>i : Fin n<VAR>k : Fin (n + 1)<GOAL>b i ∈ b.flag k ↔ i.castSucc < k
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<GOAL>Monotone b.flag
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<GOAL>IsChain (fun x x_1 => x ≤ x_1) (Set.range b.flag)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>Nontrivial R<VAR>b : Basis (Fin n) R M<GOAL>StrictMono b.flag
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>Nontrivial R<VAR>b : Basis (Fin n) R M<VAR>k : Fin (n + 1)<VAR>l : Fin n<GOAL>b.flag k ≤ LinearMap.ker (b.coord l) ↔ k ≤ l.castSucc
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>k : Fin (n + 1)<VAR>l : Fin n<VAR>h : k ≤ l.castSucc<GOAL>b.flag k ≤ LinearMap.ker (b.coord l)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>k : Fin n<GOAL>b.flag k.castSucc ≤ LinearMap.ker (b.dualBasis k)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : ℕ<VAR>b : Basis (Fin n) K V<VAR>i : Fin n<GOAL>b.flag i.castSucc ⋖ b.flag i.succ
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : ℕ<VAR>b : Basis (Fin n) K V<VAR>i : Fin n<GOAL>b.flag i.castSucc ⩿ b.flag i.succ
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : ℕ<VAR>b : Basis (Fin n) K V<GOAL>↑b.toFlag = Set.range b.flag
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : ℕ<VAR>b : Basis (Fin n) K V<VAR>p : Submodule K V<GOAL>p ∈ b.toFlag ↔ ∃ k, b.flag k = p
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : ℕ<VAR>b : Basis (Fin n) K V<GOAL>IsMaxChain (fun x x_1 => x ≤ x_1) (Set.range b.flag)
<VAR>F : Type u<VAR>K : Type v<VAR>A : Type w<VAR>DivisionRing F<VAR>DivisionRing K<VAR>AddCommGroup A<VAR>Module F K<VAR>Module K A<VAR>Module F A<VAR>IsScalarTower F K A<VAR>Nontrivial A<VAR>FiniteDimensional F A<GOAL>FiniteDimensional F K
<VAR>F : Type u<VAR>K : Type v<VAR>A : Type w<VAR>DivisionRing F<VAR>DivisionRing K<VAR>AddCommGroup A<VAR>Module F K<VAR>Module K A<VAR>Module F A<VAR>IsScalarTower F K A<VAR>hf : FiniteDimensional F A<GOAL>FiniteDimensional K A
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>Field F<VAR>Ring A<VAR>IsDomain A<VAR>Algebra F A<VAR>hp : Nat.Prime (FiniteDimensional.finrank F A)<GOAL>IsSimpleOrder (Subalgebra F A)
<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>Semiring R₁<VAR>Semiring S₁<VAR>Semiring R₂<VAR>Semiring S₂<VAR>AddCommMonoid N₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>Fintype n<VAR>Fintype m<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>DecidableEq n<VAR>DecidableEq m<VAR>f : Matrix n m N₂<VAR>i : n<VAR>j : m<GOAL>((Matrix.toLinearMap₂'Aux σ₁ σ₂ f) ((LinearMap.stdBasis R₁ (fun x => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun x => R₂) j) 1) = f i j
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>Semiring R₁<VAR>Semiring S₁<VAR>Semiring R₂<VAR>Semiring S₂<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂<VAR>b₁ : n → M₁<VAR>b₂ : m → M₂<VAR>i : n<VAR>j : m<GOAL>(LinearMap.toMatrix₂Aux R b₁ b₂) f i j = (f (b₁ i)) (b₂ j)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>Semiring R₁<VAR>Semiring S₁<VAR>Semiring R₂<VAR>Semiring S₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂<GOAL>Matrix.toLinearMap₂'Aux σ₁ σ₂ ((LinearMap.toMatrix₂Aux R (fun i => (LinearMap.stdBasis R₁ (fun x => R₁) i) 1) fun j => (LinearMap.stdBasis R₂ (fun x => R₂) j) 1) f) = f
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>Semiring R₁<VAR>Semiring S₁<VAR>Semiring R₂<VAR>Semiring S₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>f : Matrix n m N₂<GOAL>(LinearMap.toMatrix₂Aux R (fun i => (LinearMap.stdBasis R₁ (fun x => R₁) i) 1) fun j => (LinearMap.stdBasis R₂ (fun x => R₂) j) 1) (Matrix.toLinearMap₂'Aux σ₁ σ₂ f) = f
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>M : Matrix n m N₂<GOAL>Matrix.toLinearMap₂'Aux σ₁ σ₂ M = (Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>M : Matrix n m N₂<VAR>x : n → R₁<VAR>y : m → R₂<GOAL>(((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) x) y = ∑ i : n, ∑ j : m, σ₁ (x i) •> σ₂ (y j) •> M i j
<VAR>R : Type u_1<VAR>S₁ : Type u_3<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>M : Matrix n m N₂<VAR>x : n → S₁<VAR>y : m → S₂<GOAL>(((Matrix.toLinearMap₂' R) M) x) y = ∑ i : n, ∑ j : m, x i •> y j •> M i j
<VAR>n : Type u_12<VAR>m : Type u_13<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>T : Type u_17<VAR>CommSemiring T<VAR>M : Matrix n m T<VAR>v : n → T<VAR>w : m → T<GOAL>(((Matrix.toLinearMap₂' T) M) v) w = v ⬝ᵥ M *ᵥ w