ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>M : Matrix n m N₂<VAR>i : n<VAR>j : m<GOAL>(((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) ((LinearMap.stdBasis R₁ (fun x => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun x => R₂) j) 1) = M i j
<VAR>R : Type u_1<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>SMulCommClass R R N₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>M : Matrix n m N₂<VAR>i : n<VAR>j : m<GOAL>(((Matrix.toLinearMap₂' R) M) ((LinearMap.stdBasis R (fun x => R) i) 1)) ((LinearMap.stdBasis R (fun x => R) j) 1) = M i j
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<GOAL>(LinearMap.toMatrixₛₗ₂' R).symm = Matrix.toLinearMapₛₗ₂' R σ₁ σ₂
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<GOAL>(Matrix.toLinearMapₛₗ₂' R σ₁ σ₂).symm = LinearMap.toMatrixₛₗ₂' R
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂<GOAL>(Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) ((LinearMap.toMatrixₛₗ₂' R) B) = B
<VAR>R : Type u_1<VAR>S₁ : Type u_3<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>B : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂<GOAL>(Matrix.toLinearMap₂' R) ((LinearMap.toMatrix₂' R) B) = B
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>M : Matrix n m N₂<GOAL>(LinearMap.toMatrixₛₗ₂' R) ((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) = M
<VAR>R : Type u_1<VAR>S₁ : Type u_3<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>M : Matrix n m N₂<GOAL>(LinearMap.toMatrix₂' R) ((Matrix.toLinearMap₂' R) M) = M
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂<VAR>i : n<VAR>j : m<GOAL>(LinearMap.toMatrixₛₗ₂' R) B i j = (B ((LinearMap.stdBasis R₁ (fun x => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun x => R₂) j) 1)
<VAR>R : Type u_1<VAR>S₁ : Type u_3<VAR>S₂ : Type u_5<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>Semiring S₁<VAR>Semiring S₂<VAR>Module S₁ N₂<VAR>Module S₂ N₂<VAR>SMulCommClass S₁ R N₂<VAR>SMulCommClass S₂ R N₂<VAR>SMulCommClass S₂ S₁ N₂<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>B : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂<VAR>i : n<VAR>j : m<GOAL>(LinearMap.toMatrix₂' R) B i j = (B ((LinearMap.stdBasis S₁ (fun x => S₁) i) 1)) ((LinearMap.stdBasis S₂ (fun x => S₂) j) 1)
<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>R : Type u_17<VAR>CommSemiring R<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>Fintype n'<VAR>Fintype m'<VAR>DecidableEq n'<VAR>DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>l : (n' → R) →ₗ[R] n → R<VAR>r : (m' → R) →ₗ[R] m → R<GOAL>(LinearMap.toMatrix₂' R) (B.compl₁₂ l r) = (LinearMap.toMatrix' l)ᵀ * (LinearMap.toMatrix₂' R) B * LinearMap.toMatrix' r
<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>R : Type u_17<VAR>CommSemiring R<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>Fintype n'<VAR>DecidableEq n'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>f : (n' → R) →ₗ[R] n → R<GOAL>(LinearMap.toMatrix₂' R) (B ∘ₗ f) = (LinearMap.toMatrix' f)ᵀ * (LinearMap.toMatrix₂' R) B
<VAR>n : Type u_12<VAR>m : Type u_13<VAR>m' : Type u_15<VAR>R : Type u_17<VAR>CommSemiring R<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>Fintype m'<VAR>DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>f : (m' → R) →ₗ[R] m → R<GOAL>(LinearMap.toMatrix₂' R) (B.compl₂ f) = (LinearMap.toMatrix₂' R) B * LinearMap.toMatrix' f
<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>R : Type u_17<VAR>CommSemiring R<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>Fintype n'<VAR>Fintype m'<VAR>DecidableEq n'<VAR>DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>M : Matrix n' n R<VAR>N : Matrix m m' R<GOAL>M * (LinearMap.toMatrix₂' R) B * N = (LinearMap.toMatrix₂' R) (B.compl₁₂ (Matrix.toLin' Mᵀ) (Matrix.toLin' N))
<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>R : Type u_17<VAR>CommSemiring R<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>Fintype n'<VAR>DecidableEq n'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>M : Matrix n' n R<GOAL>M * (LinearMap.toMatrix₂' R) B = (LinearMap.toMatrix₂' R) (B ∘ₗ Matrix.toLin' Mᵀ)
<VAR>n : Type u_12<VAR>m : Type u_13<VAR>m' : Type u_15<VAR>R : Type u_17<VAR>CommSemiring R<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>Fintype m'<VAR>DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>M : Matrix m m' R<GOAL>(LinearMap.toMatrix₂' R) B * M = (LinearMap.toMatrix₂' R) (B.compl₂ (Matrix.toLin' M))
<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>R : Type u_17<VAR>CommSemiring R<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>DecidableEq m<VAR>Fintype n'<VAR>Fintype m'<VAR>DecidableEq n'<VAR>DecidableEq m'<VAR>M : Matrix n m R<VAR>P : Matrix n n' R<VAR>Q : Matrix m m' R<GOAL>((Matrix.toLinearMap₂' R) M).compl₁₂ (Matrix.toLin' P) (Matrix.toLin' Q) = (Matrix.toLinearMap₂' R) (Pᵀ * M * Q)
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] N₂<VAR>i : n<VAR>j : m<GOAL>(LinearMap.toMatrix₂ b₁ b₂) B i j = (B (b₁ i)) (b₂ j)
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>M : Matrix n m N₂<VAR>x : M₁<VAR>y : M₂<GOAL>(((Matrix.toLinearMap₂ b₁ b₂) M) x) y = ∑ i : n, ∑ j : m, (b₁.repr x) i •> (b₂.repr y) j •> M i j
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] N₂<GOAL>(LinearMap.toMatrix₂Aux R ⇑b₁ ⇑b₂) B = (LinearMap.toMatrix₂ b₁ b₂) B
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<GOAL>(LinearMap.toMatrix₂ b₁ b₂).symm = Matrix.toLinearMap₂ b₁ b₂
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<GOAL>(Matrix.toLinearMap₂ b₁ b₂).symm = LinearMap.toMatrix₂ b₁ b₂
<VAR>R : Type u_1<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<GOAL>Matrix.toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLinearMap₂' R
<VAR>R : Type u_1<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<GOAL>LinearMap.toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) = LinearMap.toMatrix₂' R
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] N₂<GOAL>(Matrix.toLinearMap₂ b₁ b₂) ((LinearMap.toMatrix₂ b₁ b₂) B) = B
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>M : Matrix n m N₂<GOAL>(LinearMap.toMatrix₂ b₁ b₂) ((Matrix.toLinearMap₂ b₁ b₂) M) = M
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>AddCommMonoid M₁'<VAR>Module R M₁'<VAR>AddCommMonoid M₂'<VAR>Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>Fintype n'<VAR>Fintype m'<VAR>DecidableEq n'<VAR>DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>l : M₁' →ₗ[R] M₁<VAR>r : M₂' →ₗ[R] M₂<GOAL>(LinearMap.toMatrix₂ b₁' b₂') (B.compl₁₂ l r) = ((LinearMap.toMatrix b₁' b₁) l)ᵀ * (LinearMap.toMatrix₂ b₁ b₂) B * (LinearMap.toMatrix b₂' b₂) r
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>AddCommMonoid M₁'<VAR>Module R M₁'<VAR>b₁' : Basis n' R M₁'<VAR>Fintype n'<VAR>DecidableEq n'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>f : M₁' →ₗ[R] M₁<GOAL>(LinearMap.toMatrix₂ b₁' b₂) (B ∘ₗ f) = ((LinearMap.toMatrix b₁' b₁) f)ᵀ * (LinearMap.toMatrix₂ b₁ b₂) B
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₂' : Type u_10<VAR>n : Type u_12<VAR>m : Type u_13<VAR>m' : Type u_15<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>AddCommMonoid M₂'<VAR>Module R M₂'<VAR>b₂' : Basis m' R M₂'<VAR>Fintype m'<VAR>DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>f : M₂' →ₗ[R] M₂<GOAL>(LinearMap.toMatrix₂ b₁ b₂') (B.compl₂ f) = (LinearMap.toMatrix₂ b₁ b₂) B * (LinearMap.toMatrix b₂' b₂) f
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>Fintype n'<VAR>Fintype m'<VAR>DecidableEq n'<VAR>DecidableEq m'<VAR>c₁ : Basis n' R M₁<VAR>c₂ : Basis m' R M₂<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<GOAL>(b₁.toMatrix ⇑c₁)ᵀ * (LinearMap.toMatrix₂ b₁ b₂) B * b₂.toMatrix ⇑c₂ = (LinearMap.toMatrix₂ c₁ c₂) B
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>AddCommMonoid M₁'<VAR>Module R M₁'<VAR>AddCommMonoid M₂'<VAR>Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>Fintype n'<VAR>Fintype m'<VAR>DecidableEq n'<VAR>DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>M : Matrix n' n R<VAR>N : Matrix m m' R<GOAL>M * (LinearMap.toMatrix₂ b₁ b₂) B * N = (LinearMap.toMatrix₂ b₁' b₂') (B.compl₁₂ ((Matrix.toLin b₁' b₁) Mᵀ) ((Matrix.toLin b₂' b₂) N))
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>AddCommMonoid M₁'<VAR>Module R M₁'<VAR>b₁' : Basis n' R M₁'<VAR>Fintype n'<VAR>DecidableEq n'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>M : Matrix n' n R<GOAL>M * (LinearMap.toMatrix₂ b₁ b₂) B = (LinearMap.toMatrix₂ b₁' b₂) (B ∘ₗ (Matrix.toLin b₁' b₁) Mᵀ)
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₂' : Type u_10<VAR>n : Type u_12<VAR>m : Type u_13<VAR>m' : Type u_15<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>AddCommMonoid M₂'<VAR>Module R M₂'<VAR>b₂' : Basis m' R M₂'<VAR>Fintype m'<VAR>DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>M : Matrix m m' R<GOAL>(LinearMap.toMatrix₂ b₁ b₂) B * M = (LinearMap.toMatrix₂ b₁ b₂') (B.compl₂ ((Matrix.toLin b₂' b₂) M))
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>DecidableEq n<VAR>Fintype n<VAR>DecidableEq m<VAR>Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>AddCommMonoid M₁'<VAR>Module R M₁'<VAR>AddCommMonoid M₂'<VAR>Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>Fintype n'<VAR>Fintype m'<VAR>DecidableEq n'<VAR>DecidableEq m'<VAR>M : Matrix n m R<VAR>P : Matrix n n' R<VAR>Q : Matrix m m' R<GOAL>((Matrix.toLinearMap₂ b₁ b₂) M).compl₁₂ ((Matrix.toLin b₁' b₁) P) ((Matrix.toLin b₂' b₂) Q) = (Matrix.toLinearMap₂ b₁' b₂') (Pᵀ * M * Q)
<VAR>R : Type u_1<VAR>n : Type u_12<VAR>n' : Type u_14<VAR>CommRing R<VAR>Fintype n<VAR>Fintype n'<VAR>J : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>DecidableEq n<VAR>DecidableEq n'<GOAL>((Matrix.toLinearMap₂' R) J).IsAdjointPair ((Matrix.toLinearMap₂' R) J') (Matrix.toLin' A) (Matrix.toLin' A') ↔ J.IsAdjointPair J' A A'
<VAR>R : Type u_1<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>n : Type u_12<VAR>n' : Type u_14<VAR>CommRing R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Fintype n<VAR>Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>DecidableEq n<VAR>DecidableEq n'<GOAL>((Matrix.toLinearMap₂ b₁ b₁) J).IsAdjointPair ((Matrix.toLinearMap₂ b₂ b₂) J') ((Matrix.toLin b₁ b₂) A) ((Matrix.toLin b₂ b₁) A') ↔ J.IsAdjointPair J' A A'
<VAR>R : Type u_1<VAR>n : Type u_12<VAR>CommRing R<VAR>Fintype n<VAR>J A₁ A₂ : Matrix n n R<VAR>DecidableEq n<VAR>P : Matrix n n R<VAR>h : IsUnit P<GOAL>(Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)
<VAR>R : Type u_1<VAR>n : Type u_12<VAR>CommRing R<VAR>Fintype n<VAR>J J₂ A₁ : Matrix n n R<VAR>DecidableEq n<GOAL>A₁ ∈ pairSelfAdjointMatricesSubmodule J J₂ ↔ J.IsAdjointPair J₂ A₁ A₁
<VAR>R : Type u_1<VAR>n : Type u_12<VAR>CommRing R<VAR>Fintype n<VAR>J A₁ : Matrix n n R<VAR>DecidableEq n<GOAL>A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁
<VAR>R : Type u_1<VAR>n : Type u_12<VAR>CommRing R<VAR>Fintype n<VAR>J A₁ : Matrix n n R<VAR>DecidableEq n<GOAL>A₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁
<VAR>R₁ : Type u_2<VAR>M₁ : Type u_7<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι R₁<VAR>b : Basis ι R₁ M₁<GOAL>((Matrix.toLinearMap₂' R₁) M).SeparatingLeft ↔ ((Matrix.toLinearMap₂ b b) M).SeparatingLeft
<VAR>R₁ : Type u_2<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι R₁<VAR>h : M.Nondegenerate<GOAL>((Matrix.toLinearMap₂' R₁) M).SeparatingLeft
<VAR>R₁ : Type u_2<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι R₁<GOAL>((Matrix.toLinearMap₂' R₁) M).SeparatingLeft ↔ M.Nondegenerate
<VAR>R₁ : Type u_2<VAR>M₁ : Type u_7<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι R₁<VAR>h : M.Nondegenerate<VAR>b : Basis ι R₁ M₁<GOAL>((Matrix.toLinearMap₂ b b) M).SeparatingLeft
<VAR>R₁ : Type u_2<VAR>M₁ : Type u_7<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι R₁<VAR>b : Basis ι R₁ M₁<GOAL>((Matrix.toLinearMap₂ b b) M).SeparatingLeft ↔ M.Nondegenerate
<VAR>R₁ : Type u_2<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>B : (ι → R₁) →ₗ[R₁] (ι → R₁) →ₗ[R₁] R₁<GOAL>((LinearMap.toMatrix₂' R₁) B).Nondegenerate ↔ B.SeparatingLeft
<VAR>R₁ : Type u_2<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>B : (ι → R₁) →ₗ[R₁] (ι → R₁) →ₗ[R₁] R₁<VAR>h : B.SeparatingLeft<GOAL>((LinearMap.toMatrix₂' R₁) B).Nondegenerate
<VAR>R₁ : Type u_2<VAR>M₁ : Type u_7<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁<VAR>b : Basis ι R₁ M₁<GOAL>((LinearMap.toMatrix₂ b b) B).Nondegenerate ↔ B.SeparatingLeft
<VAR>R₁ : Type u_2<VAR>M₁ : Type u_7<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁<VAR>h : B.SeparatingLeft<VAR>b : Basis ι R₁ M₁<GOAL>((LinearMap.toMatrix₂ b b) B).Nondegenerate
<VAR>R₁ : Type u_2<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>IsDomain R₁<VAR>M : Matrix ι ι R₁<GOAL>((Matrix.toLinearMap₂' R₁) M).SeparatingLeft ↔ M.det ≠ 0
<VAR>R₁ : Type u_2<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>IsDomain R₁<VAR>M : Matrix ι ι R₁<VAR>h : M.det ≠ 0<GOAL>((Matrix.toLinearMap₂' R₁) M).SeparatingLeft
<VAR>R₁ : Type u_2<VAR>M₁ : Type u_7<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>IsDomain R₁<VAR>B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁<VAR>b : Basis ι R₁ M₁<GOAL>B.SeparatingLeft ↔ ((LinearMap.toMatrix₂ b b) B).det ≠ 0
<VAR>R₁ : Type u_2<VAR>M₁ : Type u_7<VAR>ι : Type u_16<VAR>CommRing R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>DecidableEq ι<VAR>Fintype ι<VAR>IsDomain R₁<VAR>B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁<VAR>b : Basis ι R₁ M₁<VAR>h : ((LinearMap.toMatrix₂ b b) B).det ≠ 0<GOAL>B.SeparatingLeft
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<VAR>x : ↑(hs.extend ⋯)<GOAL>(Basis.extend hs) x = ↑x
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<GOAL>⇑(Basis.extend hs) = Subtype.val
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<GOAL>Set.range ⇑(Basis.extend hs) = hs.extend ⋯
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<GOAL>s ⊆ hs.extend ⋯
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>x : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(Basis.ofVectorSpace K V) x = ↑x
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<GOAL>⇑(Basis.ofVectorSpace K V) = Subtype.val
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<GOAL>LinearIndependent (ι := { x // x ∈ Basis.ofVectorSpaceIndex K V }) K Subtype.val
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<GOAL>Set.range ⇑(Basis.ofVectorSpace K V) = Basis.ofVectorSpaceIndex K V
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<GOAL>∃ s, Nonempty (Basis (↑s) K V)
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Fintype K<VAR>Fintype V<GOAL>∃ n, Fintype.card V = Fintype.card K ^ n
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : V<VAR>hv : v ≠ 0<GOAL>IsAtom (Submodule.span K {v})
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Submodule K V<GOAL>IsAtom W ↔ ∃ v, v ≠ 0 ∧ W = Submodule.span K {v}
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>AddCommGroup V'<VAR>Module K V<VAR>Module K V'<VAR>f : V →ₗ[K] V'<VAR>hf_inj : LinearMap.ker f = ⊥<GOAL>∃ g, g ∘ₗ f = LinearMap.id
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>p : Submodule K V<GOAL>∃ q, IsCompl p q
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>AddCommGroup V'<VAR>Module K V<VAR>Module K V'<VAR>f : V →ₗ[K] V'<VAR>hf_surj : LinearMap.range f = ⊤<GOAL>∃ g, f ∘ₗ g = LinearMap.id