ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>LT α<VAR>b : n → α<VAR>e : m ≃ n<GOAL>((Matrix.reindex e e) M).BlockTriangular b ↔ M.BlockTriangular (b ∘ ⇑e)
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>b : m → α<VAR>LT α<GOAL>M.BlockTriangular b → Mᵀ.BlockTriangular (⇑OrderDual.toDual ∘ b)
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>LT α<VAR>b : m → αᵒᵈ<GOAL>Mᵀ.BlockTriangular b ↔ M.BlockTriangular (⇑OrderDual.ofDual ∘ b)
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>b : m → α<VAR>LT α<GOAL>Matrix.BlockTriangular 0 b
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>b : m → α<VAR>LT α<VAR>hM : M.BlockTriangular b<GOAL>(-M).BlockTriangular b
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>LT α<VAR>hM : M.BlockTriangular b<VAR>hN : N.BlockTriangular b<GOAL>(M + N).BlockTriangular b
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>LT α<VAR>hM : M.BlockTriangular b<VAR>hN : N.BlockTriangular b<GOAL>(M - N).BlockTriangular b
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>b : m → α<VAR>Preorder α<VAR>DecidableEq m<VAR>d : m → R<GOAL>(Matrix.diagonal d).BlockTriangular b
<VAR>α : Type u_1<VAR>m' : α → Type u_6<VAR>R : Type v<VAR>CommRing R<VAR>Preorder α<VAR>DecidableEq α<VAR>d : (i : α) → Matrix (m' i) (m' i) R<GOAL>(Matrix.blockDiagonal' d).BlockTriangular Sigma.fst
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>Preorder α<VAR>DecidableEq α<VAR>d : α → Matrix m m R<GOAL>(Matrix.blockDiagonal d).BlockTriangular Prod.snd
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>b : m → α<VAR>Preorder α<VAR>DecidableEq m<GOAL>Matrix.BlockTriangular 1 b
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>b : m → α<VAR>Preorder α<VAR>DecidableEq m<VAR>i j : m<VAR>hij : b i ≤ b j<VAR>c : R<GOAL>(Matrix.stdBasisMatrix i j c).BlockTriangular b
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>b : m → α<VAR>Preorder α<VAR>DecidableEq m<VAR>i j : m<VAR>hij : b j ≤ b i<VAR>c : R<GOAL>(Matrix.stdBasisMatrix i j c).BlockTriangular (⇑OrderDual.toDual ∘ b)
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>b : m → α<VAR>Preorder α<VAR>DecidableEq m<VAR>i j : m<VAR>hij : b i ≤ b j<VAR>c : R<GOAL>(Matrix.transvection i j c).BlockTriangular b
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>b : m → α<VAR>Preorder α<VAR>DecidableEq m<VAR>i j : m<VAR>hij : b j ≤ b i<VAR>c : R<GOAL>(Matrix.transvection i j c).BlockTriangular (⇑OrderDual.toDual ∘ b)
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>b : m → α<VAR>LinearOrder α<VAR>Fintype m<VAR>M N : Matrix m m R<VAR>hM : M.BlockTriangular b<VAR>hN : N.BlockTriangular b<GOAL>(M * N).BlockTriangular b
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type v<VAR>CommRing R<VAR>Preorder α<VAR>A : Matrix m m R<VAR>B : Matrix m n R<VAR>D : Matrix n n R<VAR>a b : α<VAR>hab : a < b<GOAL>(Matrix.fromBlocks A B 0 D).BlockTriangular (Sum.elim (fun x => a) fun x => b)
<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>DecidableEq m<VAR>Fintype m<VAR>M : Matrix m m R<VAR>p q : m → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>e : ∀ (x : m), q x ↔ p x<GOAL>(M.toSquareBlockProp p).det = (M.toSquareBlockProp q).det
<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>DecidableEq m<VAR>Fintype m<VAR>M : Matrix m m R<VAR>i : m<GOAL>(M.toSquareBlock id i).det = M i i
<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>DecidableEq m<VAR>Fintype m<VAR>M : Matrix m m R<VAR>p : m → Prop<VAR>DecidablePred p<GOAL>M.det = (Matrix.fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p) (M.toBlock (fun j => ¬p j) fun j => ¬p j)).det
<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>DecidableEq m<VAR>Fintype m<VAR>M : Matrix m m R<VAR>p : m → Prop<VAR>DecidablePred p<VAR>h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0<GOAL>M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det
<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>DecidableEq m<VAR>Fintype m<VAR>M : Matrix m m R<VAR>p : m → Prop<VAR>DecidablePred p<VAR>h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0<GOAL>M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>b : m → α<VAR>DecidableEq m<VAR>Fintype m<VAR>DecidableEq α<VAR>LinearOrder α<VAR>hM : M.BlockTriangular b<GOAL>M.det = ∏ a ∈ Finset.image b Finset.univ, (M.toSquareBlock b a).det
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>b : m → α<VAR>DecidableEq m<VAR>Fintype m<VAR>DecidableEq α<VAR>Fintype α<VAR>LinearOrder α<VAR>h : M.BlockTriangular b<GOAL>M.det = ∏ k : α, (M.toSquareBlock b k).det
<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>DecidableEq m<VAR>Fintype m<VAR>LinearOrder m<VAR>h : M.BlockTriangular id<GOAL>M.det = ∏ i : m, M i i
<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>DecidableEq m<VAR>Fintype m<VAR>LinearOrder m<VAR>M : Matrix m m R<VAR>h : M.BlockTriangular ⇑OrderDual.toDual<GOAL>M.det = ∏ i : m, M i i
<VAR>R : Type v<VAR>CommRing R<VAR>n : ℕ<VAR>p : Fin n → Polynomial R<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i<GOAL>(Matrix.of fun i j => (p j).coeff ↑i).BlockTriangular id
<VAR>R : Type v<VAR>CommRing R<VAR>n : ℕ<VAR>p : Fin n → Polynomial R<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i<VAR>h_monic : ∀ (i : Fin n), (p i).Monic<GOAL>(Matrix.of fun i j => (p j).coeff ↑i).det = 1
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>b : m → α<VAR>DecidableEq m<VAR>Fintype m<VAR>LinearOrder α<VAR>Invertible M<VAR>hM : M.BlockTriangular b<VAR>k : α<GOAL>((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>b : m → α<VAR>DecidableEq m<VAR>Fintype m<VAR>LinearOrder α<VAR>Invertible M<VAR>hM : M.BlockTriangular b<VAR>k : α<GOAL>(M.toBlock (fun i => b i < k) fun i => b i < k)⁻¹ = M⁻¹.toBlock (fun i => b i < k) fun i => b i < k
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>b : m → α<VAR>DecidableEq m<VAR>Fintype m<VAR>LinearOrder α<VAR>Invertible M<VAR>hM : M.BlockTriangular b<VAR>k : α<GOAL>(M⁻¹.toBlock (fun i => k ≤ b i) fun i => b i < k) = 0
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>R : Type v<VAR>CommRing R<VAR>M : Matrix m m R<VAR>b : m → α<VAR>DecidableEq m<VAR>Fintype m<VAR>LinearOrder α<VAR>Invertible M<VAR>hM : M.BlockTriangular b<GOAL>M⁻¹.BlockTriangular b
<VAR>K : Type u<VAR>V : Type v<VAR>V' : Type v'<VAR>Ring K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>f : V →ₗ[K] V'<GOAL>f.rank ≤ Module.rank K V'
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>Ring K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>f : V →ₗ[K] V₁<GOAL>f.rank ≤ Module.rank K V
<VAR>K : Type u<VAR>V : Type v<VAR>V' : Type v'<VAR>Ring K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>Nontrivial K<GOAL>LinearMap.rank 0 = 0
<VAR>K : Type u<VAR>V : Type v<VAR>V' : Type v'<VAR>V'' : Type v''<VAR>Ring K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>AddCommGroup V''<VAR>Module K V''<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V''<GOAL>(f ∘ₗ g).rank ≤ f.rank
<VAR>K : Type u<VAR>V : Type v<VAR>V' : Type v'<VAR>V'' : Type v''<VAR>Ring K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>AddCommGroup V''<VAR>Module K V''<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V''<GOAL>Cardinal.lift.{v', v''} (f ∘ₗ g).rank ≤ Cardinal.lift.{v'', v'} g.rank
<VAR>K : Type u<VAR>V : Type v<VAR>V' : Type v'<VAR>V'' : Type v''<VAR>Ring K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>AddCommGroup V''<VAR>Module K V''<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V''<GOAL>Cardinal.lift.{v', v''} (f ∘ₗ g).rank ≤ min (Cardinal.lift.{v', v''} f.rank) (Cardinal.lift.{v'', v'} g.rank)
<VAR>K : Type u<VAR>V : Type v<VAR>V' V'₁ : Type v'<VAR>Ring K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>AddCommGroup V'₁<VAR>Module K V'₁<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V'₁<GOAL>(f ∘ₗ g).rank ≤ g.rank
<VAR>K : Type u<VAR>V : Type v<VAR>V' V'₁ : Type v'<VAR>Ring K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>AddCommGroup V'₁<VAR>Module K V'₁<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V'₁<GOAL>(f ∘ₗ g).rank ≤ min f.rank g.rank
<VAR>K : Type u<VAR>V : Type v<VAR>V' : Type v'<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>f g : V →ₗ[K] V'<GOAL>(f + g).rank ≤ f.rank + g.rank
<VAR>K : Type u<VAR>V : Type v<VAR>V' : Type v'<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>η : Type u_1<VAR>s : Finset η<VAR>f : η → V →ₗ[K] V'<GOAL>(∑ d ∈ s, f d).rank ≤ ∑ d ∈ s, (f d).rank
<VAR>K : Type u<VAR>V : Type v<VAR>V' : Type v'<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>c : Cardinal.{v'}<VAR>f : V →ₗ[K] V'<GOAL>c ≤ f.rank ↔ ∃ s, Cardinal.lift.{v', v} #↑s = Cardinal.lift.{v, v'} c ∧ LinearIndependent K fun (x : ↑s) => f ↑x
<VAR>K : Type u<VAR>V : Type v<VAR>V' : Type v'<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V'<VAR>Module K V'<VAR>n : ℕ<VAR>f : V →ₗ[K] V'<GOAL>↑n ≤ f.rank ↔ ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>h : Module.rank R M = ↑n<GOAL>FiniteDimensional.finrank R M = n
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.rank R M = 1 ↔ FiniteDimensional.finrank R M = 1
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Module.rank R M = OfNat.ofNat n ↔ FiniteDimensional.finrank R M = OfNat.ofNat n
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>h : Module.rank R M ≤ ↑n<GOAL>FiniteDimensional.finrank R M ≤ n
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>h : Module.rank R M < ↑n<GOAL>FiniteDimensional.finrank R M < n
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>h : n < FiniteDimensional.finrank R M<GOAL>↑n < Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>h : 1 < FiniteDimensional.finrank R M<GOAL>1 < Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>h : Cardinal.lift.{w, v} (Module.rank R M) ≤ Cardinal.lift.{v, w} (Module.rank R N)<VAR>h' : Module.rank R N < ℵ₀<GOAL>FiniteDimensional.finrank R M ≤ FiniteDimensional.finrank R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M ≃ₗ[R] M₂<GOAL>FiniteDimensional.finrank R M = FiniteDimensional.finrank R M₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M ≃ₗ[R] M₂<VAR>p : Submodule R M<GOAL>FiniteDimensional.finrank R ↥(Submodule.map (↑f) p) = FiniteDimensional.finrank R ↥p
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<GOAL>FiniteDimensional.finrank R ↥(LinearMap.range f) = FiniteDimensional.finrank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>q : Submodule R ↥p<GOAL>FiniteDimensional.finrank R ↥(Submodule.map p.subtype q) = FiniteDimensional.finrank R ↥q
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>FiniteDimensional.finrank R ↥⊤ = FiniteDimensional.finrank R M
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>i j : n<GOAL>Matrix.transvection i j 0 = 1
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>i j : n<VAR>Finite n<VAR>c : R<GOAL>Matrix.updateRow 1 i (1 i + c • 1 j) = Matrix.transvection i j c
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>i j : n<VAR>Fintype n<VAR>h : i ≠ j<VAR>c d : R<GOAL>Matrix.transvection i j c * Matrix.transvection i j d = Matrix.transvection i j (c + d)
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>i j : n<VAR>Fintype n<VAR>b : n<VAR>c : R<VAR>M : Matrix n n R<GOAL>(Matrix.transvection i j c * M) i b = M i b + c * M j b
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>i j : n<VAR>Fintype n<VAR>a : n<VAR>c : R<VAR>M : Matrix n n R<GOAL>(M * Matrix.transvection i j c) a j = M a j + c * M a i
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>i j : n<VAR>Fintype n<VAR>a b : n<VAR>ha : a ≠ i<VAR>c : R<VAR>M : Matrix n n R<GOAL>(Matrix.transvection i j c * M) a b = M a b
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>i j : n<VAR>Fintype n<VAR>a b : n<VAR>hb : b ≠ j<VAR>c : R<VAR>M : Matrix n n R<GOAL>(M * Matrix.transvection i j c) a b = M a b
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>i j : n<VAR>Fintype n<VAR>h : i ≠ j<VAR>c : R<GOAL>(Matrix.transvection i j c).det = 1
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>self : Matrix.TransvectionStruct n R<GOAL>self.i ≠ self.j
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>i j : n<VAR>hij : i ≠ j<VAR>c : R<GOAL>{ i := i, j := j, hij := hij, c := c }.toMatrix = Matrix.transvection i j c
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>t : Matrix.TransvectionStruct n R<GOAL>t.toMatrix.det = 1
<VAR>n : Type u_1<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>DecidableEq n<VAR>Fintype n<VAR>L : List (Matrix.TransvectionStruct n 𝕜)<GOAL>(List.map Matrix.TransvectionStruct.toMatrix L).prod.det = 1
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>CommRing R<VAR>t : Matrix.TransvectionStruct n R<GOAL>t.inv.j = t.j
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>CommRing R<VAR>t : Matrix.TransvectionStruct n R<GOAL>t.inv.i = t.i
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>CommRing R<VAR>t : Matrix.TransvectionStruct n R<GOAL>t.inv.c = -t.c
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>t : Matrix.TransvectionStruct n R<GOAL>t.inv.toMatrix * t.toMatrix = 1
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>t : Matrix.TransvectionStruct n R<GOAL>t.toMatrix * t.inv.toMatrix = 1
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>L : List (Matrix.TransvectionStruct n R)<GOAL>(List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.inv) L.reverse).prod * (List.map Matrix.TransvectionStruct.toMatrix L).prod = 1
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>L : List (Matrix.TransvectionStruct n R)<GOAL>(List.map Matrix.TransvectionStruct.toMatrix L).prod * (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.inv) L.reverse).prod = 1
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>M : Matrix n n R<VAR>hM : ∀ (t : Matrix.TransvectionStruct n R), Commute t.toMatrix M<GOAL>M ∈ Set.range ⇑(Matrix.scalar n)
<VAR>n : Type u_1<VAR>R : Type u₂<VAR>DecidableEq n<VAR>CommRing R<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (t : Matrix.TransvectionStruct n R), Commute t.toMatrix M
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>DecidableEq n<VAR>DecidableEq p<VAR>CommRing R<VAR>t : Matrix.TransvectionStruct n R<GOAL>(Matrix.TransvectionStruct.sumInl p t).toMatrix = Matrix.fromBlocks t.toMatrix 0 0 1
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>DecidableEq n<VAR>DecidableEq p<VAR>CommRing R<VAR>Fintype n<VAR>Fintype p<VAR>M : Matrix n n R<VAR>L : List (Matrix.TransvectionStruct n R)<VAR>N : Matrix p p R<GOAL>(List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.sumInl p) L).prod * Matrix.fromBlocks M 0 0 N = Matrix.fromBlocks ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M) 0 0 N
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>DecidableEq n<VAR>DecidableEq p<VAR>CommRing R<VAR>Fintype n<VAR>Fintype p<VAR>M : Matrix n n R<VAR>L : List (Matrix.TransvectionStruct n R)<VAR>N : Matrix p p R<GOAL>Matrix.fromBlocks M 0 0 N * (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.sumInl p) L).prod = Matrix.fromBlocks (M * (List.map Matrix.TransvectionStruct.toMatrix L).prod) 0 0 N
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>DecidableEq n<VAR>DecidableEq p<VAR>CommRing R<VAR>Fintype n<VAR>Fintype p<VAR>e : n ≃ p<VAR>t : Matrix.TransvectionStruct n R<GOAL>(Matrix.TransvectionStruct.reindexEquiv e t).toMatrix = (Matrix.reindexAlgEquiv R R e) t.toMatrix
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>DecidableEq n<VAR>DecidableEq p<VAR>CommRing R<VAR>Fintype n<VAR>Fintype p<VAR>e : n ≃ p<VAR>L : List (Matrix.TransvectionStruct n R)<GOAL>(List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.reindexEquiv e) L).prod = (Matrix.reindexAlgEquiv R R e) (List.map Matrix.TransvectionStruct.toMatrix L).prod
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<GOAL>(Matrix.Pivot.listTransvecCol M).length = r
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>i : Fin (Matrix.Pivot.listTransvecCol M).length<GOAL>(Matrix.Pivot.listTransvecCol M).get i = Matrix.transvection (Sum.inl (Fin.cast ⋯ i)) (Sum.inr ()) (-M (Sum.inl (Fin.cast ⋯ i)) (Sum.inr ()) / M (Sum.inr ()) (Sum.inr ()))
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<GOAL>(Matrix.Pivot.listTransvecRow M).length = r
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>i : Fin (Matrix.Pivot.listTransvecRow M).length<GOAL>(Matrix.Pivot.listTransvecRow M).get i = Matrix.transvection (Sum.inr ()) (Sum.inl (Fin.cast ⋯ i)) (-M (Sum.inr ()) (Sum.inl (Fin.cast ⋯ i)) / M (Sum.inr ()) (Sum.inr ()))
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>i : Fin r ⊕ Unit<VAR>k : ℕ<VAR>hk : k ≤ r<GOAL>((List.drop k (Matrix.Pivot.listTransvecCol M)).prod * M) (Sum.inr ()) i = M (Sum.inr ()) i
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>i : Fin r ⊕ Unit<GOAL>((Matrix.Pivot.listTransvecCol M).prod * M) (Sum.inr ()) i = M (Sum.inr ()) i
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0<VAR>i : Fin r<GOAL>((Matrix.Pivot.listTransvecCol M).prod * M) (Sum.inl i) (Sum.inr ()) = 0
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>i : Fin r ⊕ Unit<VAR>k : ℕ<VAR>hk : k ≤ r<GOAL>(M * (List.take k (Matrix.Pivot.listTransvecRow M)).prod) i (Sum.inr ()) = M i (Sum.inr ())
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>i : Fin r ⊕ Unit<GOAL>(M * (Matrix.Pivot.listTransvecRow M).prod) i (Sum.inr ()) = M i (Sum.inr ())
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0<VAR>i : Fin r<GOAL>(M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inr ()) (Sum.inl i) = 0
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0<VAR>i : Fin r<GOAL>((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inr ()) (Sum.inl i) = 0
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0<VAR>i : Fin r<GOAL>((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inl i) (Sum.inr ()) = 0
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0<GOAL>((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod).IsTwoBlockDiagonal
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0<GOAL>∃ L L', ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<GOAL>∃ L L', ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>r : ℕ<VAR>IH : ∀ (M : Matrix (Fin r) (Fin r) 𝕜), ∃ L₀ L₀' D₀, (List.map Matrix.TransvectionStruct.toMatrix L₀).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L₀').prod = Matrix.diagonal D₀<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<GOAL>∃ L L' D, (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>DecidableEq n<VAR>DecidableEq p<VAR>Fintype n<VAR>Fintype p<VAR>M : Matrix p p 𝕜<VAR>e : p ≃ n<VAR>H : ∃ L L' D, (List.map Matrix.TransvectionStruct.toMatrix L).prod * (Matrix.reindexAlgEquiv 𝕜 𝕜 e) M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D<GOAL>∃ L L' D, (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D
<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>n : Type<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n 𝕜<GOAL>∃ L L' D, (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D
<VAR>n : Type u_1<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n 𝕜<GOAL>∃ L L' D, (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D
<VAR>n : Type u_1<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n 𝕜<GOAL>∃ L L' D, M = (List.map Matrix.TransvectionStruct.toMatrix L).prod * Matrix.diagonal D * (List.map Matrix.TransvectionStruct.toMatrix L').prod
<VAR>n : Type u_1<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>DecidableEq n<VAR>Fintype n<VAR>P : Matrix n n 𝕜 → Prop<VAR>M : Matrix n n 𝕜<VAR>hdiag : ∀ (D : n → 𝕜), (Matrix.diagonal D).det = M.det → P (Matrix.diagonal D)<VAR>htransvec : ∀ (t : Matrix.TransvectionStruct n 𝕜), P t.toMatrix<VAR>hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)<GOAL>P M
<VAR>n : Type u_1<VAR>𝕜 : Type u_3<VAR>Field 𝕜<VAR>DecidableEq n<VAR>Fintype n<VAR>P : Matrix n n 𝕜 → Prop<VAR>M : Matrix n n 𝕜<VAR>hMdet : M.det ≠ 0<VAR>hdiag : ∀ (D : n → 𝕜), (Matrix.diagonal D).det ≠ 0 → P (Matrix.diagonal D)<VAR>htransvec : ∀ (t : Matrix.TransvectionStruct n 𝕜), P t.toMatrix<VAR>hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)<GOAL>P M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>self : PerfectPairing R M N<GOAL>Function.Bijective ⇑self.toLin
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>self : PerfectPairing R M N<GOAL>Function.Bijective ⇑self.toLin.flip
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<GOAL>p.flip.flip = p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<VAR>a : M<GOAL>p.toDualLeft a = p a