ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<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>b' : Basis ι' R M<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>Fintype ι'<VAR>Fintype ι<VAR>Finite κ'<VAR>DecidableEq ι<VAR>DecidableEq ι'<GOAL>(LinearMap.toMatrix b' c') f * b'.toMatrix ⇑b = (LinearMap.toMatrix b c') f
<VAR>ι : Type u_1<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>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>Fintype κ'<VAR>DecidableEq ι<VAR>DecidableEq ι'<GOAL>c.toMatrix ⇑c' * (LinearMap.toMatrix b' c') f * b'.toMatrix ⇑b = (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>Finite κ<VAR>Fintype ι<VAR>DecidableEq ι<VAR>DecidableEq ι'<VAR>b₁ : Basis ι R M<VAR>b₂ : Basis ι' R M<VAR>b₃ : Basis κ R N<VAR>A : Matrix κ ι R<GOAL>A * b₁.toMatrix ⇑b₂ = (LinearMap.toMatrix b₂ b₃) ((Matrix.toLin b₁ b₃) A)
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>CommSemiring R<VAR>Fintype ι<VAR>b : Basis ι R (ι → R)<VAR>A : Matrix ι ι R<GOAL>b.toMatrix ⇑(Pi.basisFun R ι) * A = Matrix.of fun i j => (b.repr (Aᵀ 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>Fintype ι'<VAR>Fintype ι<VAR>DecidableEq ι<VAR>DecidableEq ι'<VAR>b : Basis ι R M<VAR>v : ι' → M<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).toMatrix v = (Matrix.reindexAlgEquiv R R e) (b.toMatrix (v ∘ ⇑e))
<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>ι'' : Type u_10<VAR>Fintype ι'<VAR>b'' : ι'' → M<GOAL>b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''
<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>DecidableEq ι<VAR>Fintype ι'<GOAL>b.toMatrix ⇑b' * b'.toMatrix ⇑b = 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>b : Basis ι R M<VAR>v : ι' → M<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).toMatrix v = (b.toMatrix v).submatrix (⇑e.symm) id
<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>N : Type u_9<VAR>AddCommMonoid N<VAR>Module R N<VAR>b : Basis ι R M<VAR>f : M ≃ₗ[R] N<VAR>v : ι → N<GOAL>(b.map f).toMatrix v = b.toMatrix (⇑f.symm ∘ v)
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Zero α<VAR>DecidableEq n<VAR>d : n → α<GOAL>(Matrix.diagonal d).IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Zero α<VAR>DecidableEq n<VAR>A : Matrix n n α<VAR>h : A.IsDiag<GOAL>Matrix.diagonal A.diag = A
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Zero α<VAR>DecidableEq n<VAR>A : Matrix n n α<GOAL>A.IsDiag ↔ Matrix.diagonal A.diag = A
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Zero α<VAR>Subsingleton n<VAR>A : Matrix n n α<GOAL>A.IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Zero α<GOAL>Matrix.IsDiag 0
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>DecidableEq n<VAR>Zero α<VAR>One α<GOAL>Matrix.IsDiag 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>Zero α<VAR>Zero β<VAR>A : Matrix n n α<VAR>ha : A.IsDiag<VAR>f : α → β<VAR>hf : f 0 = 0<GOAL>(A.map f).IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup α<VAR>A : Matrix n n α<VAR>ha : A.IsDiag<GOAL>(-A).IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup α<VAR>A : Matrix n n α<GOAL>(-A).IsDiag ↔ A.IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddZeroClass α<VAR>A B : Matrix n n α<VAR>ha : A.IsDiag<VAR>hb : B.IsDiag<GOAL>(A + B).IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup α<VAR>A B : Matrix n n α<VAR>ha : A.IsDiag<VAR>hb : B.IsDiag<GOAL>(A - B).IsDiag
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>n : Type u_4<VAR>Monoid R<VAR>AddMonoid α<VAR>DistribMulAction R α<VAR>k : R<VAR>A : Matrix n n α<VAR>ha : A.IsDiag<GOAL>(k • A).IsDiag
<VAR>α : Type u_1<VAR>n : Type u_6<VAR>Semiring α<VAR>DecidableEq n<VAR>k : α<GOAL>(k • 1).IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Zero α<VAR>A : Matrix n n α<VAR>ha : A.IsDiag<GOAL>A.transpose.IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Zero α<VAR>A : Matrix n n α<GOAL>A.transpose.IsDiag ↔ A.IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Semiring α<VAR>StarRing α<VAR>A : Matrix n n α<VAR>ha : A.IsDiag<GOAL>A.conjTranspose.IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Semiring α<VAR>StarRing α<VAR>A : Matrix n n α<GOAL>A.conjTranspose.IsDiag ↔ A.IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>m : Type u_5<VAR>Zero α<VAR>A : Matrix n n α<VAR>ha : A.IsDiag<VAR>f : m → n<VAR>hf : Function.Injective f<GOAL>(A.submatrix f f).IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>m : Type u_5<VAR>MulZeroClass α<VAR>A : Matrix m m α<VAR>B : Matrix n n α<VAR>hA : A.IsDiag<VAR>hB : B.IsDiag<GOAL>(Matrix.kroneckerMap (fun x x_1 => x * x_1) A B).IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Zero α<VAR>A : Matrix n n α<VAR>h : A.IsDiag<GOAL>A.IsSymm
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>m : Type u_5<VAR>Zero α<VAR>A : Matrix m m α<VAR>D : Matrix n n α<VAR>ha : A.IsDiag<VAR>hd : D.IsDiag<GOAL>(Matrix.fromBlocks A 0 0 D).IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>m : Type u_5<VAR>Zero α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<GOAL>(Matrix.fromBlocks A B C D).IsDiag ↔ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>m : Type u_5<VAR>Zero α<VAR>A : Matrix m m α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>h : (Matrix.fromBlocks A 0 C D).IsSymm<VAR>ha : A.IsDiag<VAR>hd : D.IsDiag<GOAL>(Matrix.fromBlocks A 0 C D).IsDiag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>m : Type u_5<VAR>Fintype n<VAR>Mul α<VAR>AddCommMonoid α<VAR>A : Matrix m n α<GOAL>(A * A.transpose).IsDiag ↔ A.HasOrthogonalRows
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>m : Type u_5<VAR>Fintype m<VAR>Mul α<VAR>AddCommMonoid α<VAR>A : Matrix m n α<GOAL>(A.transpose * A).IsDiag ↔ A.HasOrthogonalCols
<VAR>n : Type u_1<VAR>R : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>σ : Equiv.Perm n<VAR>CommRing R<GOAL>(Equiv.Perm.permMatrix R σ).det = ↑↑(Equiv.Perm.sign σ)
<VAR>n : Type u_1<VAR>R : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>σ : Equiv.Perm n<VAR>AddCommMonoidWithOne R<GOAL>(Equiv.Perm.permMatrix R σ).trace = ↑(Function.fixedPoints ⇑σ).ncard
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>A : Subalgebra R S<VAR>x : R<VAR>a : ↥A<GOAL>A.lTensorBot ((algebraMap R ↥⊥) x ⊗ₜ[R] a) = x • a
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>A : Subalgebra R S<VAR>a : ↥A<GOAL>A.lTensorBot (1 ⊗ₜ[R] a) = a
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>A : Subalgebra R S<VAR>a : ↥A<GOAL>A.lTensorBot.symm a = 1 ⊗ₜ[R] a
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>A : Subalgebra R S<VAR>x : R<VAR>a : ↥A<GOAL>A.rTensorBot (a ⊗ₜ[R] (algebraMap R ↥⊥) x) = x • a
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>A : Subalgebra R S<VAR>a : ↥A<GOAL>A.rTensorBot (a ⊗ₜ[R] 1) = a
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>A : Subalgebra R S<VAR>a : ↥A<GOAL>A.rTensorBot.symm a = a ⊗ₜ[R] 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>A : Subalgebra R S<GOAL>(Algebra.TensorProduct.comm R ↥A ↥⊥).trans A.lTensorBot = A.rTensorBot
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>A : Subalgebra R S<GOAL>(Algebra.TensorProduct.comm R ↥⊥ ↥A).trans A.rTensorBot = A.lTensorBot
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>A B : Subalgebra R S<VAR>a : ↥A<VAR>b : ↥B<GOAL>(A.mulMap B) (a ⊗ₜ[R] b) = ↑a * ↑b
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>A B : Subalgebra R S<GOAL>(A.mulMap B).toLinearMap = (Subalgebra.toSubmodule A).mulMap (Subalgebra.toSubmodule B)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>A B : Subalgebra R S<GOAL>B.mulMap A = (A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>A B : Subalgebra R S<GOAL>(A.mulMap B).range = A ⊔ B
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>A : Subalgebra R S<GOAL>⊥.mulMap A = A.val.comp ↑A.lTensorBot
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>A : Subalgebra R S<GOAL>A.mulMap ⊥ = A.val.comp ↑A.rTensorBot
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>A B : Subalgebra R S<VAR>a : ↥A<VAR>b : ↥B<GOAL>↑((A.mulMap' B) (a ⊗ₜ[R] b)) = ↑a * ↑b
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>A B : Subalgebra R S<GOAL>Function.Surjective ⇑(A.mulMap' B)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A B : Subalgebra R S<VAR>Module.Free R ↥A<VAR>Module.Free R ↥B<GOAL>Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A B : Subalgebra R S<VAR>Module.Free R ↥A<VAR>Module.Free R ↥B<GOAL>FiniteDimensional.finrank R ↥(A ⊔ B) ≤ FiniteDimensional.finrank R ↥A * FiniteDimensional.finrank R ↥B
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>R : Type v<VAR>CommSemiring R<VAR>i : n<VAR>w : n → R<GOAL>LinearMap.proj i ∘ₗ Matrix.toLin' (Matrix.diagonal w) = w i • LinearMap.proj i
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>R : Type v<VAR>CommSemiring R<VAR>w : n → R<VAR>i : n<GOAL>Matrix.toLin' (Matrix.diagonal w) ∘ₗ LinearMap.stdBasis R (fun x => R) i = w i • LinearMap.stdBasis R (fun x => R) i
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>R : Type v<VAR>CommSemiring R<VAR>w : n → R<GOAL>Matrix.toLin' (Matrix.diagonal w) = LinearMap.pi fun i => w i • LinearMap.proj i
<VAR>m : Type u_1<VAR>Fintype m<VAR>K : Type u<VAR>Semifield K<VAR>DecidableEq m<VAR>w : m → K<GOAL>LinearMap.ker (Matrix.toLin' (Matrix.diagonal w)) = ⨆ i ∈ {i | w i = 0}, LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>m : Type u_1<VAR>Fintype m<VAR>K : Type u<VAR>Semifield K<VAR>DecidableEq m<VAR>w : m → K<GOAL>LinearMap.range (Matrix.toLin' (Matrix.diagonal w)) = ⨆ i ∈ {i | w i ≠ 0}, LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>m : Type u_1<VAR>Fintype m<VAR>K : Type u<VAR>Field K<VAR>DecidableEq m<VAR>DecidableEq K<VAR>w : m → K<GOAL>(Matrix.toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A B : Matrix.SpecialLinearGroup n R<GOAL>A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A B : Matrix.SpecialLinearGroup n R<GOAL>(∀ (i j : n), ↑A i j = ↑B i j) → A = B
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix n n R<VAR>h : A.det = 1<GOAL>↑⟨A, h⟩ = A
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<GOAL>↑A⁻¹ = (↑A).adjugate
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A B : Matrix.SpecialLinearGroup n R<GOAL>↑(A * B) = ↑A * ↑B
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<GOAL>(↑A).det = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<VAR>m : ℕ<GOAL>↑(A ^ m) = ↑A ^ m
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<GOAL>↑A.transpose = (↑A).transpose
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>Nontrivial R<VAR>g : Matrix.SpecialLinearGroup n R<GOAL>(↑g).det ≠ 0
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>Nontrivial R<VAR>g : Matrix.SpecialLinearGroup n R<VAR>i : n<GOAL>↑g i ≠ 0
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<VAR>v : n → R<GOAL>(Matrix.SpecialLinearGroup.toLin' A) v = (Matrix.toLin' ↑A) v
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<GOAL>↑(Matrix.SpecialLinearGroup.toLin' A) = Matrix.toLin' ↑A
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<VAR>v : n → R<GOAL>(Matrix.SpecialLinearGroup.toLin' A).symm v = (Matrix.toLin' ↑A⁻¹) v
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<GOAL>↑(Matrix.SpecialLinearGroup.toLin' A).symm = Matrix.toLin' ↑A⁻¹
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<GOAL>Function.Injective ⇑Matrix.SpecialLinearGroup.toLin'
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<GOAL>↑(Matrix.SpecialLinearGroup.toGL A) = ↑(Matrix.SpecialLinearGroup.toLin' A)
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>g : Matrix.SpecialLinearGroup n R<GOAL>↑((Matrix.SpecialLinearGroup.map f) g) = f.mapMatrix ↑g
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>Subsingleton n<GOAL>Subgroup.center (Matrix.SpecialLinearGroup n R) = ⊥
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<VAR>hA : A ∈ Subgroup.center (Matrix.SpecialLinearGroup n R)<VAR>i : n<GOAL>(Matrix.scalar n) (↑A i i) = ↑A
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : ↥(Subgroup.center (Matrix.SpecialLinearGroup n R))<VAR>i : n<GOAL>(Matrix.scalar n) (↑↑A i i) = ↑↑A
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup n R<GOAL>A ∈ Subgroup.center (Matrix.SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (Matrix.scalar n) r = ↑A
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>i : n<VAR>a : ↥(rootsOfUnity (Fintype.card n).toPNat' R)<GOAL>↑↑((Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' i).symm a) = a • 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>i : n<VAR>A : ↥(Subgroup.center (Matrix.SpecialLinearGroup n R))<GOAL>(Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' i) A = rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>g : Matrix.SpecialLinearGroup n ℤ<GOAL>↑((Matrix.SpecialLinearGroup.map (Int.castRingHom R)) g) = (↑g).map ⇑(Int.castRingHom R)
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>Fact (Even (Fintype.card n))<VAR>g : Matrix.SpecialLinearGroup n R<GOAL>↑(-g) = -↑g
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>Fact (Even (Fintype.card n))<VAR>g : Matrix.SpecialLinearGroup n ℤ<GOAL>(Matrix.SpecialLinearGroup.map (Int.castRingHom R)) (-g) = -(Matrix.SpecialLinearGroup.map (Int.castRingHom R)) g
<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup (Fin 2) R<GOAL>Matrix.det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1
<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup (Fin 2) R<GOAL>A⁻¹ = ⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩
<VAR>R : Type v<VAR>CommRing R<VAR>P : Matrix.SpecialLinearGroup (Fin 2) R → Prop<VAR>h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩<VAR>g : Matrix.SpecialLinearGroup (Fin 2) R<GOAL>P g
<VAR>R : Type u_2<VAR>Field R<VAR>g : Matrix.SpecialLinearGroup (Fin 2) R<VAR>hg : ↑g 1 0 = 0<GOAL>∃ a b, ∃ (h : a ≠ 0), g = ⟨!![a, b; 0, a⁻¹], ⋯⟩
<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup (Fin 2) R<VAR>i : Fin 2<GOAL>IsCoprime (↑A i 0) (↑A i 1)
<VAR>R : Type v<VAR>CommRing R<VAR>A : Matrix.SpecialLinearGroup (Fin 2) R<VAR>j : Fin 2<GOAL>IsCoprime (↑A 0 j) (↑A 1 j)
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R<VAR>hab : IsCoprime a b<VAR>j : Fin 2<GOAL>∃ g, ↑g 0 j = a ∧ ↑g 1 j = b
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R<VAR>hab : IsCoprime a b<VAR>i : Fin 2<GOAL>∃ g, ↑g i 0 = a ∧ ↑g i 1 = b
<VAR>R : Type u_1<VAR>CommRing R<VAR>v : Fin 2 → R<VAR>hab : IsCoprime (v 0) (v 1)<VAR>A : Matrix.SpecialLinearGroup (Fin 2) R<GOAL>IsCoprime (Matrix.vecMul v (↑A) 0) (Matrix.vecMul v (↑A) 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>v : Fin 2 → R<VAR>hab : IsCoprime (v 0) (v 1)<VAR>A : Matrix.SpecialLinearGroup (Fin 2) R<GOAL>IsCoprime ((↑A).mulVec v 0) ((↑A).mulVec v 1)
<GOAL>↑ModularGroup.S = !![0, -1; 1, 0]
<GOAL>↑ModularGroup.T = !![1, 1; 0, 1]
<GOAL>↑ModularGroup.T⁻¹ = !![1, -1; 0, 1]
<VAR>n : ℤ<GOAL>↑(ModularGroup.T ^ n) = !![1, n; 0, 1]
<VAR>n : ℤ<VAR>g : Matrix.SpecialLinearGroup (Fin 2) ℤ<GOAL>↑(ModularGroup.T ^ n * g) 1 = ↑g 1
<VAR>g : Matrix.SpecialLinearGroup (Fin 2) ℤ<GOAL>↑(ModularGroup.T * g) 1 = ↑g 1
<VAR>g : Matrix.SpecialLinearGroup (Fin 2) ℤ<GOAL>↑(ModularGroup.T⁻¹ * g) 1 = ↑g 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>M : Matrix (Fin (n + 1)) (Fin n) R<VAR>hv : ∑ j : Fin (n + 1), M j = 0<VAR>j₁ j₂ : Fin (n + 1)<GOAL>(M.submatrix j₁.succAbove id).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix j₂.succAbove id).det
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>M : Matrix (Fin n) (Fin (n + 1)) R<VAR>hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0<VAR>j₁ j₂ : Fin (n + 1)<GOAL>(M.submatrix id j₁.succAbove).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Star α<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<GOAL>A.conjTranspose = A
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Star α<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<GOAL>IsSelfAdjoint A
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Star α<VAR>A : Matrix n n α<GOAL>(∀ (i j : n), star (A j i) = A i j) → A.IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Star α<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<VAR>i j : n<GOAL>star (A j i) = A i j
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Star α<VAR>A : Matrix n n α<GOAL>A.IsHermitian ↔ ∀ (i j : n), star (A j i) = A i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>Star α<VAR>Star β<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<VAR>f : α → β<VAR>hf : Function.Semiconj f star star<GOAL>(A.map f).IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Star α<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<GOAL>A.transpose.IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Star α<VAR>A : Matrix n n α<GOAL>A.transpose.IsHermitian ↔ A.IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Star α<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<GOAL>A.conjTranspose.IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Star α<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<VAR>f : m → n<GOAL>(A.submatrix f f).IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Star α<VAR>A : Matrix n n α<VAR>e : m ≃ n<GOAL>(A.submatrix ⇑e ⇑e).IsHermitian ↔ A.IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>InvolutiveStar α<VAR>A : Matrix n n α<GOAL>A.conjTranspose.IsHermitian ↔ A.IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>InvolutiveStar α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>hA : A.IsHermitian<VAR>hBC : B.conjTranspose = C<VAR>hD : D.IsHermitian<GOAL>(Matrix.fromBlocks A B C D).IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>InvolutiveStar α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<GOAL>(Matrix.fromBlocks A B C D).IsHermitian ↔ A.IsHermitian ∧ B.conjTranspose = C ∧ C.conjTranspose = B ∧ D.IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>DecidableEq n<VAR>v : n → α<VAR>h : IsSelfAdjoint v<GOAL>(Matrix.diagonal v).IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>DecidableEq n<VAR>d : n → α<GOAL>(Matrix.diagonal d).IsHermitian ↔ ∀ (i : n), IsSelfAdjoint (d i)
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>TrivialStar α<VAR>DecidableEq n<VAR>v : n → α<GOAL>(Matrix.diagonal v).IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddMonoid α<VAR>StarAddMonoid α<GOAL>Matrix.IsHermitian 0
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>A B : Matrix n n α<VAR>hA : A.IsHermitian<VAR>hB : B.IsHermitian<GOAL>(A + B).IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddCommMonoid α<VAR>StarAddMonoid α<VAR>A : Matrix n n α<GOAL>(A + A.conjTranspose).IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddCommMonoid α<VAR>StarAddMonoid α<VAR>A : Matrix n n α<GOAL>(A.conjTranspose + A).IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup α<VAR>StarAddMonoid α<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<GOAL>(-A).IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup α<VAR>StarAddMonoid α<VAR>A B : Matrix n n α<VAR>hA : A.IsHermitian<VAR>hB : B.IsHermitian<GOAL>(A - B).IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>NonUnitalSemiring α<VAR>StarRing α<VAR>Fintype n<VAR>A : Matrix m n α<GOAL>(A * A.conjTranspose).IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>NonUnitalSemiring α<VAR>StarRing α<VAR>Fintype m<VAR>A : Matrix m n α<GOAL>(A.conjTranspose * A).IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>NonUnitalSemiring α<VAR>StarRing α<VAR>Fintype m<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>hA : A.IsHermitian<GOAL>(B.conjTranspose * A * B).IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>NonUnitalSemiring α<VAR>StarRing α<VAR>Fintype m<VAR>A : Matrix m m α<VAR>B : Matrix n m α<VAR>hA : A.IsHermitian<GOAL>(B * A * B.conjTranspose).IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>NonUnitalSemiring α<VAR>StarRing α<VAR>Fintype n<VAR>A B : Matrix n n α<VAR>hA : A.IsHermitian<VAR>hB : B.IsHermitian<GOAL>Commute A B ↔ (A * B).IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Semiring α<VAR>StarRing α<VAR>DecidableEq n<GOAL>Matrix.IsHermitian 1
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Semiring α<VAR>StarRing α<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<VAR>k : ℕ<GOAL>(A ^ k).IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>CommRing α<VAR>StarRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m α<VAR>hA : A.IsHermitian<GOAL>A⁻¹.IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>CommRing α<VAR>StarRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m α<VAR>Invertible A<GOAL>A⁻¹.IsHermitian ↔ A.IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>CommRing α<VAR>StarRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m α<VAR>hA : A.IsHermitian<GOAL>A.adjugate.IsHermitian
<VAR>α : Type u_1<VAR>m : Type u_3<VAR>CommRing α<VAR>StarRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m α<VAR>h : A.IsHermitian<VAR>k : ℤ<GOAL>(A ^ k).IsHermitian
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>RCLike α<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<VAR>i : n<GOAL>↑(RCLike.re (A i i)) = A i i
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>RCLike α<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<GOAL>(fun i => ↑(RCLike.re (A.diag i))) = A.diag
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>RCLike α<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n α<GOAL>A.IsHermitian ↔ (Matrix.toEuclideanLin A).IsSymmetric
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Zero β<VAR>AddCommMonoid M<VAR>DistribSMul R M<VAR>v : α →₀ β<VAR>c : R<VAR>h : α → β → M<GOAL>c • v.sum h = v.sum fun a b => c • h a b