ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype n<VAR>v : n → α<VAR>A : Matrix m n α<GOAL>A *ᵥ -v = -(A *ᵥ v)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype n<VAR>v : n → α<VAR>A : Matrix m n α<GOAL>-A *ᵥ -v = A *ᵥ v
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype n<VAR>A : Matrix m n α<VAR>x y : n → α<GOAL>A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype n<VAR>A B : Matrix m n α<VAR>x : n → α<GOAL>(A - B) *ᵥ x = A *ᵥ x - B *ᵥ x
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype m<VAR>A B : Matrix m n α<VAR>x : m → α<GOAL>x ᵥ* (A - B) = x ᵥ* A - x ᵥ* B
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype m<VAR>A : Matrix m n α<VAR>x y : m → α<GOAL>(x - y) ᵥ* A = x ᵥ* A - y ᵥ* A
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalCommSemiring α<VAR>Fintype m<VAR>A : Matrix m n α<VAR>x : m → α<GOAL>Aᵀ *ᵥ x = x ᵥ* A
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalCommSemiring α<VAR>Fintype n<VAR>A : Matrix m n α<VAR>x : n → α<GOAL>x ᵥ* Aᵀ = A *ᵥ x
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalCommSemiring α<VAR>Fintype n<VAR>Fintype o<VAR>A : Matrix m n α<VAR>B : Matrix o n α<VAR>x : o → α<GOAL>A *ᵥ x ᵥ* B = (A * Bᵀ) *ᵥ x
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalCommSemiring α<VAR>Fintype m<VAR>Fintype n<VAR>A : Matrix m n α<VAR>B : Matrix m o α<VAR>x : n → α<GOAL>(A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>CommSemiring α<VAR>Fintype n<VAR>A : Matrix m n α<VAR>b : n → α<VAR>a : α<GOAL>A *ᵥ a • b = a • A *ᵥ b
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>x : ℤ<VAR>v : m → α<GOAL>↑x *ᵥ v = ↑x • v
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>x : ℤ<VAR>v : m → α<GOAL>v ᵥ* ↑x = MulOpposite.op ↑x • v
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<GOAL>Mᵀᵀ = M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<GOAL>Function.Injective Matrix.transpose
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>A B : Matrix m n α<GOAL>Aᵀ = Bᵀ ↔ A = B
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>M : Matrix n n α<VAR>v : n → α<GOAL>Mᵀ = Matrix.diagonal v ↔ M = Matrix.diagonal v
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Zero α<GOAL>0ᵀ = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Zero α<VAR>M : Matrix m n α<GOAL>Mᵀ = 0 ↔ M = 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<GOAL>1ᵀ = 1
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>M : Matrix n n α<GOAL>Mᵀ = 1 ↔ M = 1
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>AddMonoidWithOne α<VAR>d : ℕ<GOAL>(↑d)ᵀ = ↑d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>AddMonoidWithOne α<VAR>M : Matrix n n α<VAR>d : ℕ<GOAL>Mᵀ = ↑d ↔ M = ↑d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>AddMonoidWithOne α<VAR>d : ℕ<VAR>d.AtLeastTwo<GOAL>(OfNat.ofNat d)ᵀ = OfNat.ofNat d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>AddMonoidWithOne α<VAR>M : Matrix n n α<VAR>d : ℕ<VAR>d.AtLeastTwo<GOAL>Mᵀ = OfNat.ofNat d ↔ M = OfNat.ofNat d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>AddGroupWithOne α<VAR>d : ℤ<GOAL>(↑d)ᵀ = ↑d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>AddGroupWithOne α<VAR>M : Matrix n n α<VAR>d : ℤ<GOAL>Mᵀ = ↑d ↔ M = ↑d
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Add α<VAR>M N : Matrix m n α<GOAL>(M + N)ᵀ = Mᵀ + Nᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Sub α<VAR>M N : Matrix m n α<GOAL>(M - N)ᵀ = Mᵀ - Nᵀ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddCommMonoid α<VAR>CommSemigroup α<VAR>Fintype n<VAR>M : Matrix m n α<VAR>N : Matrix n l α<GOAL>(M * N)ᵀ = Nᵀ * Mᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>R : Type u_10<VAR>SMul R α<VAR>c : R<VAR>M : Matrix m n α<GOAL>(c • M)ᵀ = c • Mᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Neg α<VAR>M : Matrix m n α<GOAL>(-M)ᵀ = -Mᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>f : α → β<VAR>M : Matrix m n α<GOAL>Mᵀ.map f = (M.map f)ᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Add α<VAR>M : Matrix m n α<GOAL>(Matrix.transposeAddEquiv m n α) M = Mᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Add α<GOAL>(Matrix.transposeAddEquiv m n α).symm = Matrix.transposeAddEquiv n m α
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddMonoid α<VAR>l : List (Matrix m n α)<GOAL>l.sumᵀ = (List.map Matrix.transpose l).sum
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddCommMonoid α<VAR>s : Multiset (Matrix m n α)<GOAL>s.sumᵀ = (Multiset.map Matrix.transpose s).sum
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddCommMonoid α<VAR>ι : Type u_10<VAR>s : Finset ι<VAR>M : ι → Matrix m n α<GOAL>(∑ i ∈ s, M i)ᵀ = ∑ i ∈ s, (M i)ᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Semiring R<VAR>AddCommMonoid α<VAR>Module R α<GOAL>∀ (a : Matrix m n α), (Matrix.transposeLinearEquiv m n R α) a = (Matrix.transposeAddEquiv m n α).toFun a
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Semiring R<VAR>AddCommMonoid α<VAR>Module R α<GOAL>(Matrix.transposeLinearEquiv m n R α).symm = Matrix.transposeLinearEquiv n m R α
<VAR>m : Type u_2<VAR>α : Type v<VAR>AddCommMonoid α<VAR>CommSemigroup α<VAR>Fintype m<VAR>M : (Matrix m m α)ᵐᵒᵖ<GOAL>(Matrix.transposeRingEquiv m α).symm M = (MulOpposite.unop M)ᵀ
<VAR>m : Type u_2<VAR>α : Type v<VAR>AddCommMonoid α<VAR>CommSemigroup α<VAR>Fintype m<VAR>M : Matrix m m α<GOAL>(Matrix.transposeRingEquiv m α) M = MulOpposite.op Mᵀ
<VAR>m : Type u_2<VAR>α : Type v<VAR>CommSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>M : Matrix m m α<VAR>k : ℕ<GOAL>(M ^ k)ᵀ = Mᵀ ^ k
<VAR>m : Type u_2<VAR>α : Type v<VAR>CommSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>l : List (Matrix m m α)<GOAL>l.prodᵀ = (List.map Matrix.transpose l).reverse.prod
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>CommSemiring R<VAR>CommSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>Algebra R α<GOAL>∀ (a : (Matrix m m α)ᵐᵒᵖ), (Matrix.transposeAlgEquiv m R α).symm a = ((Matrix.transposeAddEquiv m m α).trans MulOpposite.opAddEquiv).invFun a
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>CommSemiring R<VAR>CommSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>Algebra R α<VAR>M : Matrix m m α<GOAL>(Matrix.transposeAlgEquiv m R α) M = MulOpposite.op Mᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Star α<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>Mᴴ j i = star (M i j)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>InvolutiveStar α<VAR>M : Matrix m n α<GOAL>Mᴴᴴ = M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>InvolutiveStar α<GOAL>Function.Injective Matrix.conjTranspose
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>InvolutiveStar α<VAR>A B : Matrix m n α<GOAL>Aᴴ = Bᴴ ↔ A = B
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>M : Matrix n n α<VAR>v : n → α<GOAL>Mᴴ = Matrix.diagonal v ↔ M = Matrix.diagonal (star v)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddMonoid α<VAR>StarAddMonoid α<GOAL>0ᴴ = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>M : Matrix m n α<GOAL>Mᴴ = 0 ↔ M = 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Semiring α<VAR>StarRing α<GOAL>1ᴴ = 1
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Semiring α<VAR>StarRing α<VAR>M : Matrix n n α<GOAL>Mᴴ = 1 ↔ M = 1
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Semiring α<VAR>StarRing α<VAR>d : ℕ<GOAL>(↑d)ᴴ = ↑d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Semiring α<VAR>StarRing α<VAR>M : Matrix n n α<VAR>d : ℕ<GOAL>Mᴴ = ↑d ↔ M = ↑d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Semiring α<VAR>StarRing α<VAR>d : ℕ<VAR>d.AtLeastTwo<GOAL>(OfNat.ofNat d)ᴴ = OfNat.ofNat d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Semiring α<VAR>StarRing α<VAR>M : Matrix n n α<VAR>d : ℕ<VAR>d.AtLeastTwo<GOAL>Mᴴ = OfNat.ofNat d ↔ M = OfNat.ofNat d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Ring α<VAR>StarRing α<VAR>d : ℤ<GOAL>(↑d)ᴴ = ↑d
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Ring α<VAR>StarRing α<VAR>M : Matrix n n α<VAR>d : ℤ<GOAL>Mᴴ = ↑d ↔ M = ↑d
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>M N : Matrix m n α<GOAL>(M + N)ᴴ = Mᴴ + Nᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddGroup α<VAR>StarAddMonoid α<VAR>M N : Matrix m n α<GOAL>(M - N)ᴴ = Mᴴ - Nᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Star R<VAR>Star α<VAR>SMul R α<VAR>StarModule R α<VAR>c : R<VAR>M : Matrix m n α<GOAL>(c • M)ᴴ = star c • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Star R<VAR>Star α<VAR>SMul R α<VAR>SMul Rᵐᵒᵖ α<VAR>c : R<VAR>M : Matrix m n α<VAR>h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a<GOAL>(c • M)ᴴ = MulOpposite.op (star c) • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Mul α<VAR>StarMul α<VAR>c : α<VAR>M : Matrix m n α<GOAL>(c • M)ᴴ = MulOpposite.op (star c) • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>c : ℕ<VAR>M : Matrix m n α<GOAL>(c • M)ᴴ = c • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddGroup α<VAR>StarAddMonoid α<VAR>c : ℤ<VAR>M : Matrix m n α<GOAL>(c • M)ᴴ = c • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Semiring R<VAR>AddCommMonoid α<VAR>StarAddMonoid α<VAR>Module R α<VAR>c : ℕ<VAR>M : Matrix m n α<GOAL>(↑c • M)ᴴ = ↑c • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Semiring R<VAR>AddCommMonoid α<VAR>StarAddMonoid α<VAR>Module R α<VAR>c : ℕ<VAR>c.AtLeastTwo<VAR>M : Matrix m n α<GOAL>(OfNat.ofNat c • M)ᴴ = OfNat.ofNat c • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Ring R<VAR>AddCommGroup α<VAR>StarAddMonoid α<VAR>Module R α<VAR>c : ℤ<VAR>M : Matrix m n α<GOAL>(↑c • M)ᴴ = ↑c • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>DivisionSemiring R<VAR>AddCommMonoid α<VAR>StarAddMonoid α<VAR>Module R α<VAR>c : ℕ<VAR>M : Matrix m n α<GOAL>((↑c)⁻¹ • M)ᴴ = (↑c)⁻¹ • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>DivisionSemiring R<VAR>AddCommMonoid α<VAR>StarAddMonoid α<VAR>Module R α<VAR>c : ℕ<VAR>c.AtLeastTwo<VAR>M : Matrix m n α<GOAL>((OfNat.ofNat c)⁻¹ • M)ᴴ = (OfNat.ofNat c)⁻¹ • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>DivisionRing R<VAR>AddCommGroup α<VAR>StarAddMonoid α<VAR>Module R α<VAR>c : ℤ<VAR>M : Matrix m n α<GOAL>((↑c)⁻¹ • M)ᴴ = (↑c)⁻¹ • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>DivisionRing R<VAR>AddCommGroup α<VAR>StarAddMonoid α<VAR>Module R α<VAR>c : ℚ<VAR>M : Matrix m n α<GOAL>(↑c • M)ᴴ = ↑c • Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddCommGroup α<VAR>StarAddMonoid α<VAR>Module ℚ α<VAR>c : ℚ<VAR>M : Matrix m n α<GOAL>(c • M)ᴴ = c • Mᴴ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype n<VAR>NonUnitalSemiring α<VAR>StarRing α<VAR>M : Matrix m n α<VAR>N : Matrix n l α<GOAL>(M * N)ᴴ = Nᴴ * Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddGroup α<VAR>StarAddMonoid α<VAR>M : Matrix m n α<GOAL>(-M)ᴴ = -Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>Star α<VAR>Star β<VAR>A : Matrix m n α<VAR>f : α → β<VAR>hf : Function.Semiconj f star star<GOAL>Aᴴ.map f = (A.map f)ᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Star α<VAR>TrivialStar α<VAR>A : Matrix m n α<GOAL>Aᴴ = Aᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>M : Matrix m n α<GOAL>(Matrix.conjTransposeAddEquiv m n α) M = Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddMonoid α<VAR>StarAddMonoid α<GOAL>(Matrix.conjTransposeAddEquiv m n α).symm = Matrix.conjTransposeAddEquiv n m α
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>l : List (Matrix m n α)<GOAL>l.sumᴴ = (List.map Matrix.conjTranspose l).sum
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddCommMonoid α<VAR>StarAddMonoid α<VAR>s : Multiset (Matrix m n α)<GOAL>s.sumᴴ = (Multiset.map Matrix.conjTranspose s).sum
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddCommMonoid α<VAR>StarAddMonoid α<VAR>ι : Type u_10<VAR>s : Finset ι<VAR>M : ι → Matrix m n α<GOAL>(∑ i ∈ s, M i)ᴴ = ∑ i ∈ s, (M i)ᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>AddCommMonoid α<VAR>StarAddMonoid α<VAR>Module R α<VAR>StarModule R α<GOAL>∀ (a : Matrix m n α), (Matrix.conjTransposeLinearEquiv m n R α) a = (Matrix.conjTransposeAddEquiv m n α).toFun a
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>AddCommMonoid α<VAR>StarAddMonoid α<VAR>Module R α<VAR>StarModule R α<GOAL>(Matrix.conjTransposeLinearEquiv m n R α).symm = Matrix.conjTransposeLinearEquiv n m R α
<VAR>m : Type u_2<VAR>α : Type v<VAR>Semiring α<VAR>StarRing α<VAR>Fintype m<VAR>M : (Matrix m m α)ᵐᵒᵖ<GOAL>(Matrix.conjTransposeRingEquiv m α).symm M = (MulOpposite.unop M)ᴴ
<VAR>m : Type u_2<VAR>α : Type v<VAR>Semiring α<VAR>StarRing α<VAR>Fintype m<VAR>M : Matrix m m α<GOAL>(Matrix.conjTransposeRingEquiv m α) M = MulOpposite.op Mᴴ
<VAR>m : Type u_2<VAR>α : Type v<VAR>Semiring α<VAR>StarRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>M : Matrix m m α<VAR>k : ℕ<GOAL>(M ^ k)ᴴ = Mᴴ ^ k
<VAR>m : Type u_2<VAR>α : Type v<VAR>Semiring α<VAR>StarRing α<VAR>Fintype m<VAR>DecidableEq m<VAR>l : List (Matrix m m α)<GOAL>l.prodᴴ = (List.map Matrix.conjTranspose l).reverse.prod
<VAR>m : Type u_2<VAR>α : Type v<VAR>Star α<VAR>M : Matrix m m α<GOAL>star M = Mᴴ
<VAR>n : Type u_3<VAR>α : Type v<VAR>Star α<VAR>M : Matrix n n α<VAR>i j : n<GOAL>star M i j = star (M j i)
<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype n<VAR>NonUnitalSemiring α<VAR>StarRing α<VAR>M N : Matrix n n α<GOAL>star (M * N) = star N * star M
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>A : Matrix m n α<VAR>r_reindex : l → m<VAR>c_reindex : o → n<VAR>i : l<VAR>j : o<GOAL>A.submatrix r_reindex c_reindex i j = A (r_reindex i) (c_reindex j)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>A : Matrix m n α<GOAL>A.submatrix id id = A
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>l₂ : Type u_10<VAR>o₂ : Type u_11<VAR>A : Matrix m n α<VAR>r₁ : l → m<VAR>c₁ : o → n<VAR>r₂ : l₂ → l<VAR>c₂ : o₂ → o<GOAL>(A.submatrix r₁ c₁).submatrix r₂ c₂ = A.submatrix (r₁ ∘ r₂) (c₁ ∘ c₂)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>A : Matrix m n α<VAR>r_reindex : l → m<VAR>c_reindex : o → n<GOAL>(A.submatrix r_reindex c_reindex)ᵀ = Aᵀ.submatrix c_reindex r_reindex
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Star α<VAR>A : Matrix m n α<VAR>r_reindex : l → m<VAR>c_reindex : o → n<GOAL>(A.submatrix r_reindex c_reindex)ᴴ = Aᴴ.submatrix c_reindex r_reindex
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Add α<VAR>A B : Matrix m n α<GOAL>(A + B).submatrix = A.submatrix + B.submatrix
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Neg α<VAR>A : Matrix m n α<GOAL>(-A).submatrix = -A.submatrix
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Sub α<VAR>A B : Matrix m n α<GOAL>(A - B).submatrix = A.submatrix - B.submatrix
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Zero α<GOAL>Matrix.submatrix 0 = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>R : Type u_10<VAR>SMul R α<VAR>r : R<VAR>A : Matrix m n α<GOAL>(r • A).submatrix = r • A.submatrix
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>β : Type w<VAR>f : α → β<VAR>e₁ : l → m<VAR>e₂ : o → n<VAR>A : Matrix m n α<GOAL>(A.map f).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type v<VAR>Zero α<VAR>DecidableEq m<VAR>DecidableEq l<VAR>d : m → α<VAR>e : l → m<VAR>he : Function.Injective e<GOAL>(Matrix.diagonal d).submatrix e e = Matrix.diagonal (d ∘ e)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type v<VAR>Zero α<VAR>One α<VAR>DecidableEq m<VAR>DecidableEq l<VAR>e : l → m<VAR>he : Function.Injective e<GOAL>Matrix.submatrix 1 e e = 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Fintype n<VAR>Fintype o<VAR>Mul α<VAR>AddCommMonoid α<VAR>p : Type u_10<VAR>q : Type u_11<VAR>M : Matrix m n α<VAR>N : Matrix n p α<VAR>e₁ : l → m<VAR>e₂ : o → n<VAR>e₃ : q → p<VAR>he₂ : Function.Bijective e₂<GOAL>(M * N).submatrix e₁ e₃ = M.submatrix e₁ e₂ * N.submatrix e₂ e₃
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type v<VAR>A : Matrix m m α<VAR>e : l → m<GOAL>(A.submatrix e e).diag = A.diag ∘ e
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type v<VAR>Zero α<VAR>DecidableEq m<VAR>DecidableEq l<VAR>d : m → α<VAR>e : l ↪ m<GOAL>(Matrix.diagonal d).submatrix ⇑e ⇑e = Matrix.diagonal (d ∘ ⇑e)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type v<VAR>Zero α<VAR>DecidableEq m<VAR>DecidableEq l<VAR>d : m → α<VAR>e : l ≃ m<GOAL>(Matrix.diagonal d).submatrix ⇑e ⇑e = Matrix.diagonal (d ∘ ⇑e)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type v<VAR>Zero α<VAR>One α<VAR>DecidableEq m<VAR>DecidableEq l<VAR>e : l ↪ m<GOAL>Matrix.submatrix 1 ⇑e ⇑e = 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type v<VAR>Zero α<VAR>One α<VAR>DecidableEq m<VAR>DecidableEq l<VAR>e : l ≃ m<GOAL>Matrix.submatrix 1 ⇑e ⇑e = 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Fintype n<VAR>Fintype o<VAR>AddCommMonoid α<VAR>Mul α<VAR>p : Type u_10<VAR>q : Type u_11<VAR>M : Matrix m n α<VAR>N : Matrix n p α<VAR>e₁ : l → m<VAR>e₂ : o ≃ n<VAR>e₃ : q → p<GOAL>M.submatrix e₁ ⇑e₂ * N.submatrix (⇑e₂) e₃ = (M * N).submatrix e₁ e₃
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Fintype n<VAR>Fintype o<VAR>NonUnitalNonAssocSemiring α<VAR>M : Matrix m n α<VAR>v : o → α<VAR>e₁ : l → m<VAR>e₂ : o ≃ n<GOAL>M.submatrix e₁ ⇑e₂ *ᵥ v = (M *ᵥ v ∘ ⇑e₂.symm) ∘ e₁
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Fintype l<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>M : Matrix m n α<VAR>v : l → α<VAR>e₁ : l ≃ m<VAR>e₂ : o → n<GOAL>v ᵥ* M.submatrix (⇑e₁) e₂ = (v ∘ ⇑e₁.symm ᵥ* M) ∘ e₂
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Fintype n<VAR>Finite o<VAR>NonAssocSemiring α<VAR>DecidableEq o<VAR>e₁ : n ≃ o<VAR>e₂ : l → o<VAR>M : Matrix m n α<GOAL>M * Matrix.submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Fintype m<VAR>Finite o<VAR>NonAssocSemiring α<VAR>DecidableEq o<VAR>e₁ : l → o<VAR>e₂ : m ≃ o<VAR>M : Matrix m n α<GOAL>Matrix.submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>eₘ : m ≃ l<VAR>eₙ : n ≃ o<VAR>M : Matrix m n α<GOAL>(Matrix.reindex eₘ eₙ) M = M.submatrix ⇑eₘ.symm ⇑eₙ.symm
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>A : Matrix m n α<GOAL>(Matrix.reindex (Equiv.refl m) (Equiv.refl n)) A = A
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>eₘ : m ≃ l<VAR>eₙ : n ≃ o<GOAL>(Matrix.reindex eₘ eₙ).symm = Matrix.reindex eₘ.symm eₙ.symm
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>l₂ : Type u_10<VAR>o₂ : Type u_11<VAR>eₘ : m ≃ l<VAR>eₙ : n ≃ o<VAR>eₘ₂ : l ≃ l₂<VAR>eₙ₂ : o ≃ o₂<GOAL>(Matrix.reindex eₘ eₙ).trans (Matrix.reindex eₘ₂ eₙ₂) = Matrix.reindex (eₘ.trans eₘ₂) (eₙ.trans eₙ₂)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>eₘ : m ≃ l<VAR>eₙ : n ≃ o<VAR>M : Matrix m n α<GOAL>((Matrix.reindex eₘ eₙ) M)ᵀ = (Matrix.reindex eₙ eₘ) Mᵀ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Star α<VAR>eₘ : m ≃ l<VAR>eₙ : n ≃ o<VAR>M : Matrix m n α<GOAL>((Matrix.reindex eₘ eₙ) M)ᴴ = (Matrix.reindex eₙ eₘ) Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype m<VAR>Fintype n<VAR>AddCommMonoid α<VAR>Mul α<VAR>e : m ≃ n<VAR>M : Matrix m n α<GOAL>M.submatrix id ⇑e * Mᵀ.submatrix (⇑e) id = M * Mᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>β : Type w<VAR>Fintype n<VAR>NonAssocSemiring α<VAR>NonAssocSemiring β<VAR>M : Matrix m n α<VAR>N : Matrix n o α<VAR>i : m<VAR>j : o<VAR>f : α →+* β<GOAL>f ((M * N) i j) = (M.map ⇑f * N.map ⇑f) i j
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>S : Type u_8<VAR>Fintype n<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>v w : n → R<GOAL>f (v ⬝ᵥ w) = ⇑f ∘ v ⬝ᵥ ⇑f ∘ w
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>S : Type u_8<VAR>Fintype n<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>M : Matrix n m R<VAR>v : n → R<VAR>i : m<GOAL>f ((v ᵥ* M) i) = (⇑f ∘ v ᵥ* M.map ⇑f) i
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>S : Type u_8<VAR>Fintype n<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>M : Matrix m n R<VAR>v : n → R<VAR>i : m<GOAL>f ((M *ᵥ v) i) = (M.map ⇑f *ᵥ ⇑f ∘ v) i
<VAR>n : ℕ<GOAL>Function.Injective BitVec.toNat
<VAR>n : ℕ<GOAL>Function.Injective BitVec.toFin
<VAR>w : ℕ<VAR>n : ℕ<VAR>x : BitVec w<GOAL>(n • x).toFin = n • x.toFin
<VAR>w : ℕ<VAR>z : ℤ<VAR>x : BitVec w<GOAL>(z • x).toFin = z • x.toFin
<VAR>w : ℕ<VAR>x : BitVec w<VAR>n : ℕ<GOAL>(x ^ n).toFin = x.toFin ^ n
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<GOAL>(Tuple.graph f).card = n
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<GOAL>Tuple.graph.proj ∘ ⇑(Tuple.graphEquiv₁ f) = f
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<VAR>i : Fin n<GOAL>(Tuple.graphEquiv₂ f) i = (Tuple.graphEquiv₁ f) ((Tuple.sort f) i)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<GOAL>f ∘ ⇑(Tuple.sort f) = Tuple.graph.proj ∘ ⇑(Tuple.graphEquiv₂ f)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<GOAL>Monotone Tuple.graph.proj
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<GOAL>Monotone (f ∘ ⇑(Tuple.sort f))
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>DecidableRel LE.le<VAR>m : ℕ<VAR>f : Fin m → α<VAR>a : α<VAR>h_sorted : Monotone f<VAR>j : Fin m<GOAL>↑j < Fintype.card { i // f i ≤ a } ↔ f j ≤ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>DecidableRel LE.le<VAR>m : ℕ<VAR>f : Fin m → α<VAR>a : α<VAR>h_sorted : Antitone f<VAR>j : Fin m<GOAL>↑j < Fintype.card { i // a ≤ f i } ↔ a ≤ f j
<VAR>n : ℕ<VAR>α : Type u_1<VAR>PartialOrder α<VAR>f : Fin n → α<VAR>σ τ : Equiv.Perm (Fin n)<VAR>hfσ : Monotone (f ∘ ⇑σ)<VAR>hfτ : Monotone (f ∘ ⇑τ)<GOAL>f ∘ ⇑σ = f ∘ ⇑τ
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>σ = Tuple.sort f ↔ StrictMono ⇑(Equiv.trans σ (Tuple.graphEquiv₁ f))
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>σ = Tuple.sort f ↔ Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<GOAL>Tuple.sort f = Equiv.refl (Fin n) ↔ Monotone f
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>f ∘ ⇑σ = f ∘ ⇑(Tuple.sort f) ↔ Monotone (f ∘ ⇑σ)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>(f ∘ ⇑σ) ∘ ⇑(Tuple.sort (f ∘ ⇑σ)) = f ∘ ⇑(Tuple.sort f)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<VAR>h : f ∘ ⇑σ ≠ f ∘ ⇑(Tuple.sort f)<GOAL>∃ i j, i < j ∧ (f ∘ ⇑σ) j < (f ∘ ⇑σ) i
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<VAR>h : f ≠ f ∘ ⇑(Tuple.sort f)<GOAL>∃ i j, i < j ∧ f j < f i