ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>Module B M<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Algebra A B<VAR>IsScalarTower A B M<VAR>m : M<VAR>n : N<VAR>a : A<GOAL>(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M N) (m ⊗ₜ[A] a ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] n
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>Module B M<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Algebra A B<VAR>IsScalarTower A B M<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M N).symm (m ⊗ₜ[R] n) = m ⊗ₜ[A] 1 ⊗ₜ[R] n
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>m : M<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.AlgebraTensorModule.leftComm R A M P Q) (m ⊗ₜ[A] p ⊗ₜ[R] q) = p ⊗ₜ[A] m ⊗ₜ[R] q
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>m : M<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.AlgebraTensorModule.leftComm R A M P Q).symm (p ⊗ₜ[A] m ⊗ₜ[R] q) = m ⊗ₜ[A] p ⊗ₜ[R] q
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid P<VAR>Module A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>m : M<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.AlgebraTensorModule.rightComm R A M P Q) ((m ⊗ₜ[A] p) ⊗ₜ[R] q) = (m ⊗ₜ[R] q) ⊗ₜ[A] p
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid P<VAR>Module A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>m : M<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.AlgebraTensorModule.rightComm R A M P Q).symm ((m ⊗ₜ[R] q) ⊗ₜ[A] p) = (m ⊗ₜ[A] p) ⊗ₜ[R] q
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>m : M<VAR>n : N<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M N P Q) ((m ⊗ₜ[R] n) ⊗ₜ[A] p ⊗ₜ[R] q) = (m ⊗ₜ[A] p) ⊗ₜ[R] n ⊗ₜ[R] q
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>m : M<VAR>n : N<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M N P Q).symm ((m ⊗ₜ[A] p) ⊗ₜ[R] n ⊗ₜ[R] q) = (m ⊗ₜ[R] n) ⊗ₜ[A] p ⊗ₜ[R] q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Submodule.baseChange A ⊥ = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Submodule.baseChange A ⊤ = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>a : A<VAR>m : M<VAR>hm : m ∈ p<GOAL>a ⊗ₜ[R] m ∈ Submodule.baseChange A p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>Submodule.baseChange A (Submodule.span R s) = Submodule.span A (⇑((TensorProduct.mk R A M) 1) '' s)
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A.det<VAR>Invertible A<GOAL>⅟A = ⅟A.det • A.adjugate
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<VAR>Invertible A.det<GOAL>(⅟A).det = ⅟A.det
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A.det<GOAL>A.invertibleEquivDetInvertible.symm inst✝ = A.invertibleOfDetInvertible
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<GOAL>A.invertibleEquivDetInvertible inst✝ = A.detInvertibleOfInvertible
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<GOAL>A * B = 1 ↔ B * A = 1
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>IsUnit A ↔ IsUnit A.det
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : (Matrix n n α)ˣ<GOAL>IsUnit (↑A).det
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<GOAL>IsUnit A.det
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>h : B * A = 1<GOAL>IsUnit A
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>(∃ B, B * A = 1) ↔ IsUnit A
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>h : A * B = 1<GOAL>IsUnit A
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>(∃ B, A * B = 1) ↔ IsUnit A
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>h : B * A = 1<GOAL>IsUnit A.det
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>h : A * B = 1<GOAL>IsUnit A.det
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>Nontrivial α<VAR>h : B * A = 1<GOAL>A.det ≠ 0
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>Nontrivial α<VAR>h : A * B = 1<GOAL>A.det ≠ 0
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : IsUnit A.det<GOAL>IsUnit A.transpose.det
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A⁻¹ = Ring.inverse A.det • A.adjugate
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : ¬IsUnit A.det<GOAL>A⁻¹ = 0
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A⁻¹ = ↑h.unit⁻¹ • A.adjugate
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<GOAL>⅟A = A⁻¹
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : (Matrix n n α)ˣ<GOAL>↑A⁻¹ = (↑A)⁻¹
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A⁻¹ = Ring.inverse A
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A⁻¹.transpose = A.transpose⁻¹
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>StarRing α<GOAL>A⁻¹.conjTranspose = A.conjTranspose⁻¹
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A * A⁻¹ = 1
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A⁻¹ * A = 1
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<GOAL>A⁻¹⁻¹ = A
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>B : Matrix m n α<VAR>h : IsUnit A.det<GOAL>B * A * A⁻¹ = B
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>B : Matrix n m α<VAR>h : IsUnit A.det<GOAL>A * (A⁻¹ * B) = B
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>B : Matrix m n α<VAR>h : IsUnit A.det<GOAL>B * A⁻¹ * A = B
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>B : Matrix n m α<VAR>h : IsUnit A.det<GOAL>A⁻¹ * (A * B) = B
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<GOAL>A * A⁻¹ = 1
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<GOAL>A⁻¹ * A = 1
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>B : Matrix m n α<VAR>Invertible A<GOAL>B * A * A⁻¹ = B
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>B : Matrix n m α<VAR>Invertible A<GOAL>A * (A⁻¹ * B) = B
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>B : Matrix m n α<VAR>Invertible A<GOAL>B * A⁻¹ * A = B
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>B : Matrix n m α<VAR>Invertible A<GOAL>A⁻¹ * (A * B) = B
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B C : Matrix n n α<VAR>Invertible A<GOAL>A⁻¹ * B = C ↔ B = A * C
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B C : Matrix n n α<VAR>Invertible A<GOAL>B * A⁻¹ = C ↔ B = C * A
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<VAR>u v : n → α<VAR>hM : u = A.mulVec v<GOAL>A⁻¹.mulVec u = v
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<GOAL>Function.Injective fun x => A * x
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<GOAL>Function.Injective fun x => x * A
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<VAR>x y : Matrix n m α<GOAL>A * x = A * y ↔ x = y
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A<VAR>x y : Matrix m n α<GOAL>x * A = y * A ↔ x = y
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq m<VAR>CommRing α<VAR>A : Matrix m n α<VAR>B : Matrix n m α<VAR>h : A * B = 1<GOAL>Function.Injective fun x => x * A
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq m<VAR>CommRing α<VAR>A : Matrix m n α<VAR>B : Matrix n m α<VAR>h : A * B = 1<GOAL>Function.Injective fun x => B * x
<VAR>m : Type u<VAR>n : Type u'<VAR>DecidableEq n<VAR>R : Type u_2<VAR>Semiring R<VAR>Fintype m<VAR>Finite n<VAR>A : Matrix m n R<GOAL>(Function.Surjective fun v => Matrix.vecMul v A) ↔ ∃ B, B * A = 1
<VAR>m : Type u<VAR>n : Type u'<VAR>DecidableEq m<VAR>R : Type u_2<VAR>Semiring R<VAR>Finite m<VAR>Fintype n<VAR>A : Matrix m n R<GOAL>Function.Surjective A.mulVec ↔ ∃ B, A * B = 1
<VAR>m : Type u<VAR>DecidableEq m<VAR>R : Type u_2<VAR>CommRing R<VAR>Fintype m<VAR>A : Matrix m m R<GOAL>(Function.Surjective fun v => Matrix.vecMul v A) ↔ IsUnit A
<VAR>m : Type u<VAR>DecidableEq m<VAR>R : Type u_2<VAR>CommRing R<VAR>Fintype m<VAR>A : Matrix m m R<GOAL>Function.Surjective A.mulVec ↔ IsUnit A
<VAR>m : Type u<VAR>DecidableEq m<VAR>K : Type u_3<VAR>Field K<VAR>Fintype m<VAR>A : Matrix m m K<GOAL>(Function.Injective fun v => Matrix.vecMul v A) ↔ IsUnit A
<VAR>m : Type u<VAR>DecidableEq m<VAR>K : Type u_3<VAR>Field K<VAR>Fintype m<VAR>A : Matrix m m K<GOAL>Function.Injective A.mulVec ↔ IsUnit A
<VAR>m : Type u<VAR>DecidableEq m<VAR>K : Type u_3<VAR>Field K<VAR>Fintype m<VAR>A : Matrix m m K<GOAL>(LinearIndependent K fun i => A i) ↔ IsUnit A
<VAR>m : Type u<VAR>DecidableEq m<VAR>K : Type u_3<VAR>Field K<VAR>Fintype m<VAR>A : Matrix m m K<GOAL>(LinearIndependent K fun i => A.transpose i) ↔ IsUnit A
<VAR>m : Type u<VAR>DecidableEq m<VAR>R : Type u_2<VAR>CommRing R<VAR>Fintype m<VAR>A : Matrix m m R<VAR>Invertible A<GOAL>Function.Surjective fun v => Matrix.vecMul v A
<VAR>m : Type u<VAR>DecidableEq m<VAR>R : Type u_2<VAR>CommRing R<VAR>Fintype m<VAR>A : Matrix m m R<VAR>Invertible A<GOAL>Function.Surjective A.mulVec
<VAR>m : Type u<VAR>DecidableEq m<VAR>K : Type u_3<VAR>Field K<VAR>Fintype m<VAR>A : Matrix m m K<VAR>Invertible A<GOAL>Function.Injective fun v => Matrix.vecMul v A
<VAR>m : Type u<VAR>DecidableEq m<VAR>K : Type u_3<VAR>Field K<VAR>Fintype m<VAR>A : Matrix m m K<VAR>Invertible A<GOAL>Function.Injective A.mulVec
<VAR>m : Type u<VAR>DecidableEq m<VAR>K : Type u_3<VAR>Field K<VAR>Fintype m<VAR>A : Matrix m m K<VAR>Invertible A<GOAL>LinearIndependent K fun i => A i
<VAR>m : Type u<VAR>DecidableEq m<VAR>K : Type u_3<VAR>Field K<VAR>Fintype m<VAR>A : Matrix m m K<VAR>Invertible A<GOAL>LinearIndependent K fun i => A.transpose i
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A⁻¹.det * A.det = 1
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A⁻¹.det = Ring.inverse A.det
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : IsUnit A.det<GOAL>IsUnit A⁻¹.det
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A⁻¹⁻¹ = A
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>IsUnit A⁻¹.det ↔ IsUnit A.det
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>Invertible A.det<GOAL>A.unitOfDetInvertible = A.nonsingInvUnit ⋯
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>h : B * A = 1<GOAL>A⁻¹ = B
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>h : A * B = 1<GOAL>A⁻¹ = B
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B C : Matrix n n α<VAR>h : B * A = 1<VAR>g : C * A = 1<GOAL>B = C
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B C : Matrix n n α<VAR>h : A * B = 1<VAR>g : A * C = 1<GOAL>B = C
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B C : Matrix n n α<VAR>h : A * B = 1<VAR>g : C * A = 1<GOAL>B = C
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>h : A⁻¹ = B⁻¹<VAR>h' : IsUnit A.det<GOAL>A = B
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<GOAL>0⁻¹ = 0
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>k : α<VAR>Invertible k<VAR>h : IsUnit A.det<GOAL>(k • A)⁻¹ = ⅟k • A⁻¹
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>k : αˣ<VAR>h : IsUnit A.det<GOAL>(k • A)⁻¹ = k⁻¹ • A⁻¹
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A.adjugate⁻¹ = h.unit⁻¹ • A
<VAR>n : Type u'<VAR>Fintype n<VAR>DecidableEq n<VAR>α : Type u_2<VAR>Semiring α<VAR>v : n → α<VAR>Invertible v<VAR>Invertible (Matrix.diagonal v)<GOAL>⅟(Matrix.diagonal v) = Matrix.diagonal ⅟v
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>v : n → α<VAR>Invertible (Matrix.diagonal v)<GOAL>(Matrix.diagonalInvertibleEquivInvertible v) inst✝ = Matrix.invertibleOfDiagonalInvertible v
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>v : n → α<VAR>Invertible v<GOAL>(Matrix.diagonalInvertibleEquivInvertible v).symm inst✝ = Matrix.diagonalInvertible v
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>v : n → α<GOAL>IsUnit (Matrix.diagonal v) ↔ IsUnit v
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>v : n → α<GOAL>(Matrix.diagonal v)⁻¹ = Matrix.diagonal (Ring.inverse v)
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>A⁻¹⁻¹⁻¹ = A⁻¹
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A ↔ IsUnit B<GOAL>A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A ↔ IsUnit B<GOAL>A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A B : Matrix n n α<GOAL>(A * B)⁻¹ = B⁻¹ * A⁻¹
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>l : List (Matrix n n α)<GOAL>l.prod⁻¹ = (List.map Inv.inv l.reverse).prod
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>h : IsUnit A.det<GOAL>A.det • A⁻¹.mulVec b = A.cramer b
<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>h : IsUnit A.det<GOAL>A.det • Matrix.vecMul b A⁻¹ = A.transpose.cramer b
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m α<VAR>e₁ e₂ : n ≃ m<VAR>Invertible A<VAR>Invertible (A.submatrix ⇑e₁ ⇑e₂)<GOAL>⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m α<VAR>e₁ e₂ : n ≃ m<GOAL>∀ (x : Invertible (A.submatrix ⇑e₁ ⇑e₂)), (A.submatrixEquivInvertibleEquivInvertible e₁ e₂) x = A.invertibleOfSubmatrixEquivInvertible e₁ e₂
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m α<VAR>e₁ e₂ : n ≃ m<GOAL>∀ (x : Invertible A), (A.submatrixEquivInvertibleEquivInvertible e₁ e₂).symm x = A.submatrixEquivInvertible e₁ e₂
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m α<VAR>e₁ e₂ : n ≃ m<GOAL>IsUnit (A.submatrix ⇑e₁ ⇑e₂) ↔ IsUnit A
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m α<VAR>e₁ e₂ : n ≃ m<GOAL>(A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁
<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>e₁ e₂ : n ≃ m<VAR>A : Matrix n n α<GOAL>((Matrix.reindex e₁ e₂) A)⁻¹ = (Matrix.reindex e₂ e₁) A⁻¹
<VAR>m : Type u<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>CommRing α<VAR>M : Matrix m m α<VAR>h : IsUnit M<VAR>N : Matrix m m α<GOAL>(M * N * M⁻¹).det = N.det
<VAR>m : Type u<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>CommRing α<VAR>M : Matrix m m α<VAR>h : IsUnit M<VAR>N : Matrix m m α<GOAL>(M⁻¹ * N * M).det = N.det
<VAR>n : Type u_1<VAR>Fintype n<VAR>R : Type u_2<VAR>CommRing R<VAR>DecidableEq n<VAR>P : Matrix n n R<VAR>h : Invertible P<GOAL>↑(P.toLinearEquiv' h) = Matrix.toLin' P
<VAR>n : Type u_1<VAR>Fintype n<VAR>R : Type u_2<VAR>CommRing R<VAR>DecidableEq n<VAR>P : Matrix n n R<VAR>h : Invertible P<GOAL>↑(P.toLinearEquiv' h).symm = Matrix.toLin' ⅟P
<VAR>n : Type u_1<VAR>Fintype n<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>b : Basis n R M<VAR>DecidableEq n<VAR>A : Matrix n n R<VAR>hA : IsUnit A.det<VAR>a : M<GOAL>(Matrix.toLinearEquiv b A hA) a = ((Matrix.toLin b b) A) a
<VAR>n : Type u_1<VAR>Fintype n<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>b : Basis n R M<VAR>DecidableEq n<VAR>A : Matrix n n R<VAR>hA : IsUnit A.det<GOAL>LinearMap.ker ((Matrix.toLin b b) A) = ⊥
<VAR>n : Type u_1<VAR>Fintype n<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>b : Basis n R M<VAR>DecidableEq n<VAR>A : Matrix n n R<VAR>hA : IsUnit A.det<GOAL>LinearMap.range ((Matrix.toLin b b) A) = ⊤
<VAR>n : Type u_1<VAR>Fintype n<VAR>K : Type u_4<VAR>DecidableEq n<VAR>Field K<VAR>M : Matrix n n K<GOAL>(∃ v, v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0
<VAR>n : Type u_1<VAR>Fintype n<VAR>A : Type u_4<VAR>K : Type u_5<VAR>DecidableEq n<VAR>CommRing A<VAR>Nontrivial A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>M : Matrix n n A<GOAL>(∃ v, v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0
<VAR>n : Type u_1<VAR>Fintype n<VAR>A : Type u_4<VAR>DecidableEq n<VAR>CommRing A<VAR>IsDomain A<VAR>M : Matrix n n A<GOAL>(∃ v, v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0
<VAR>n : Type u_1<VAR>Fintype n<VAR>A : Type u_4<VAR>DecidableEq n<VAR>CommRing A<VAR>IsDomain A<VAR>M : Matrix n n A<GOAL>(∃ v, v ≠ 0 ∧ Matrix.vecMul v M = 0) ↔ M.det = 0
<VAR>n : Type u_1<VAR>Fintype n<VAR>A : Type u_4<VAR>DecidableEq n<VAR>CommRing A<VAR>IsDomain A<VAR>M : Matrix n n A<GOAL>M.Nondegenerate ↔ M.det ≠ 0
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>S : Type u_2<VAR>LinearOrderedCommRing S<VAR>A : Matrix n n S<VAR>h1 : Pairwise fun i j => A i j < 0<VAR>h2 : ∀ (j : n), 0 < ∑ i : n, A i j<GOAL>A.det ≠ 0
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>S : Type u_2<VAR>LinearOrderedCommRing S<VAR>A : Matrix n n S<VAR>h1 : Pairwise fun i j => A i j < 0<VAR>h2 : ∀ (i : n), 0 < ∑ j : n, A i j<GOAL>A.det ≠ 0
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<GOAL>(spectrum ℝ A).Finite
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>a : Matrix n n 𝕜<VAR>ha : a.IsHermitian<GOAL>spectrum ℝ a = Set.range ha.eigenvalues
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>g : C(↑(spectrum ℝ A), ℝ)<GOAL>hA.cfcAux g = ↑hA.eigenvectorUnitary * Matrix.diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<GOAL>ClosedEmbedding ⇑hA.cfcAux
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<GOAL>hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) = A
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f : ℝ → ℝ<GOAL>cfc f A = hA.cfc f
<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>b : m → α<VAR>LT α<VAR>f : n → m<VAR>h : M.BlockTriangular b<GOAL>(M.submatrix f f).BlockTriangular (b ∘ f)