SesquilinearForm

📁 Source: Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

Statistics

Metric	Count
Definitions toMatrix₂, toMatrix₂', toMatrix₂Aux, toMatrixₛₗ₂', IsAdjointPair, IsSelfAdjoint, IsSkewAdjoint, toLinearMap₂, toLinearMap₂', toLinearMap₂'Aux, toLinearMapₛₗ₂, toLinearMapₛₗ₂', pairSelfAdjointMatricesSubmodule, selfAdjointMatricesSubmodule, skewAdjointMatricesSubmodule	15
Theorems toMatrix₂, toMatrix₂', toMatrix₂, toMatrix₂', toMatrix₂, toMatrix₂', mul_toMatrix', mul_toMatrix₂, mul_toMatrix₂'_mul, mul_toMatrix₂_mul, nondegenerate_iff_det_ne_zero, nondegenerate_of_det_ne_zero, nondegenerate_toLinearMap₂'_iff_det_ne_zero, nondegenerate_toLinearMap₂'_of_det_ne_zero', nondegenerate_toMatrix₂'_iff, nondegenerate_toMatrix₂_iff, separatingLeft_iff_det_ne_zero, separatingLeft_of_det_ne_zero, separatingLeft_toLinearMap₂'_iff_det_ne_zero, separatingLeft_toLinearMap₂'_of_det_ne_zero', separatingLeft_toMatrix₂'_iff, separatingLeft_toMatrix₂_iff, separatingRight_iff_det_ne_zero, separatingRight_of_det_ne_zero, separatingRight_toLinearMap₂'_iff_det_ne_zero, separatingRight_toLinearMap₂'_of_det_ne_zero', separatingRight_toMatrix₂'_iff, separatingRight_toMatrix₂_iff, toLinearMap₂'Aux_toMatrix₂Aux, toMatrix'_toLinearMap₂', toMatrix'_toLinearMapₛₗ₂', toMatrix₂'_apply, toMatrix₂'_comp, toMatrix₂'_compl₁₂, toMatrix₂'_compl₂, toMatrix₂'_mul, toMatrix₂Aux_apply, toMatrix₂Aux_eq, toMatrix₂_apply, toMatrix₂_basisFun, toMatrix₂_comp, toMatrix₂_compl₁₂, toMatrix₂_compl₂, toMatrix₂_mul, toMatrix₂_mul_basis_toMatrix, toMatrix₂_symm, toMatrix₂_symm', toMatrix₂_toLinearMap₂, toMatrix₂_toLinearMapₛₗ₂, toMatrixₛₗ₂'_apply, toMatrixₛₗ₂'_symm, toLinearMap₂, toLinearMap₂', toLinearMap₂, toLinearMap₂', toLinearMap₂, toLinearMap₂', isAdjointPair_equiv, nondegenerate_toLinearMap₂'_iff, nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂, nondegenerate_toLinearMap₂_iff, separatingLeft_toLinearMap₂'_iff, separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂, separatingLeft_toLinearMap₂_iff, separatingRight_toLinearMap₂'_iff, separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂, separatingRight_toLinearMap₂_iff, toLinearMap₂'Aux_single, toLinearMap₂'_apply, toLinearMap₂'_apply', toLinearMap₂'_comp, toLinearMap₂'_single, toLinearMap₂'_toMatrix', toLinearMap₂_apply, toLinearMap₂_apply_basis, toLinearMap₂_basisFun, toLinearMap₂_compl₁₂, toLinearMap₂_symm, toLinearMap₂_toMatrix₂, toLinearMapₛₗ₂'_apply, toLinearMapₛₗ₂'_aux_eq, toLinearMapₛₗ₂'_single, toLinearMapₛₗ₂'_symm, toLinearMapₛₗ₂'_toMatrix', toLinearMapₛₗ₂_apply, toLinearMapₛₗ₂_apply_basis, toLinearMapₛₗ₂_symm, toLinearMapₛₗ₂_toMatrix₂, toMatrix₂Aux_toLinearMap₂'Aux, apply_eq_dotProduct_toMatrix₂_mulVec, dotProduct_toMatrix₂_mulVec, isAdjointPair_toLinearMap₂, isAdjointPair_toLinearMap₂', mem_pairSelfAdjointMatricesSubmodule, mem_selfAdjointMatricesSubmodule, mem_skewAdjointMatricesSubmodule	96
Total	111

LinearMap

Definitions

Name	Category	Theorems
toMatrix₂ 📖	CompOp	30 math math: toMatrix₂_mul, Matrix.toLinearMap₂_toMatrix₂, star_dotProduct_toMatrix₂_mulVec, toMatrix₂_toLinearMapₛₗ₂, toMatrix₂_compl₂, isPosSemidef_iff_posSemidef_toMatrix, toMatrix₂_comp, apply_eq_dotProduct_toMatrix₂_mulVec, toMatrix₂_basisFun, mul_toMatrix₂, SeparatingRight.toMatrix₂, apply_eq_star_dotProduct_toMatrix₂_mulVec, toMatrix₂_compl₁₂, toMatrix₂_toLinearMap₂, toMatrix₂Aux_eq, toMatrix₂_symm, SeparatingLeft.toMatrix₂, Matrix.toLinearMap₂_symm, mul_toMatrix₂_mul, Matrix.toLinearMapₛₗ₂_symm, toMatrix₂_mul_basis_toMatrix, toMatrix₂_apply, nondegenerate_toMatrix₂_iff, toMatrix₂_symm', separatingRight_toMatrix₂_iff, separatingLeft_toMatrix₂_iff, Nondegenerate.toMatrix₂, Matrix.toLinearMapₛₗ₂_toMatrix₂, dotProduct_toMatrix₂_mulVec, isSymm_iff_isHermitian_toMatrix
toMatrix₂' 📖	CompOp	16 math math: SeparatingRight.toMatrix₂', separatingRight_toMatrix₂'_iff, toMatrix₂'_compl₁₂, separatingLeft_toMatrix₂'_iff, mul_toMatrix', toMatrix₂_basisFun, Matrix.toLinearMap₂'_toMatrix', toMatrix'_toLinearMap₂', nondegenerate_toMatrix₂'_iff, mul_toMatrix₂'_mul, toMatrix₂'_mul, Nondegenerate.toMatrix₂', toMatrix₂'_compl₂, toMatrix₂'_comp, SeparatingLeft.toMatrix₂', toMatrix₂'_apply
toMatrix₂Aux 📖	CompOp	4 math math: Matrix.toMatrix₂Aux_toLinearMap₂'Aux, toMatrix₂Aux_eq, toMatrix₂Aux_apply, toLinearMap₂'Aux_toMatrix₂Aux
toMatrixₛₗ₂' 📖	CompOp	5 math math: toMatrixₛₗ₂'_symm, Matrix.toLinearMapₛₗ₂'_symm, Matrix.toLinearMapₛₗ₂'_toMatrix', toMatrix'_toLinearMapₛₗ₂', toMatrixₛₗ₂'_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_toMatrix' 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Pi.addCommMonoid Pi.Function.module Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' comp RingHomCompTriple.ids Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction Matrix.toLin' Matrix.transpose	—	Algebra.to_smulCommClass RingHomInvPair.ids instSMulCommClass RingHomCompTriple.ids Function.smulCommClass toMatrix₂'_comp toMatrix'_toLin' Matrix.transpose_transpose
mul_toMatrix₂ 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ comp Algebra.to_smulCommClass Algebra.id RingHomCompTriple.ids Matrix.toLin Finite.of_fintype Matrix.transpose	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass RingHomCompTriple.ids Finite.of_fintype toMatrix₂_comp toMatrix_toLin Matrix.transpose_transpose
mul_toMatrix₂'_mul 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Pi.addCommMonoid Pi.Function.module Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' compl₁₂ Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction Matrix.toLin' Matrix.transpose	—	Algebra.to_smulCommClass RingHomInvPair.ids instSMulCommClass Function.smulCommClass toMatrix₂'_compl₁₂ toMatrix'_toLin' Matrix.transpose_transpose
mul_toMatrix₂_mul 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ compl₁₂ Algebra.to_smulCommClass Algebra.id Matrix.toLin Finite.of_fintype Matrix.transpose	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass Finite.of_fintype toMatrix₂_compl₁₂ toMatrix_toLin Matrix.transpose_transpose
nondegenerate_iff_det_ne_zero 📖	mathematical	—	Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass Finite.of_fintype Matrix.nondegenerate_iff_det_ne_zero nondegenerate_toMatrix₂_iff
nondegenerate_of_det_ne_zero 📖	mathematical	—	Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass nondegenerate_iff_det_ne_zero
nondegenerate_toLinearMap₂'_iff_det_ne_zero 📖	mathematical	—	Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module Algebra.to_smulCommClass Algebra.id instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂'	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass instSMulCommClass Finite.of_fintype Matrix.nondegenerate_toLinearMap₂'_iff Matrix.nondegenerate_iff_det_ne_zero
nondegenerate_toLinearMap₂'_of_det_ne_zero' 📖	mathematical	—	Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module Algebra.to_smulCommClass Algebra.id instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂'	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass instSMulCommClass nondegenerate_toLinearMap₂'_iff_det_ne_zero
nondegenerate_toMatrix₂'_iff 📖	mathematical	—	Matrix.Nondegenerate Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' Nondegenerate	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids instSMulCommClass smulCommClass_self Matrix.nondegenerate_toLinearMap₂'_iff Matrix.toLinearMap₂'_toMatrix'
nondegenerate_toMatrix₂_iff 📖	mathematical	—	Matrix.Nondegenerate Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ Nondegenerate	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids smulCommClass_self instSMulCommClass Matrix.nondegenerate_toLinearMap₂_iff Matrix.toLinearMap₂_toMatrix₂
separatingLeft_iff_det_ne_zero 📖	mathematical	—	SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass Finite.of_fintype Matrix.separatingLeft_iff_det_ne_zero separatingLeft_toMatrix₂_iff
separatingLeft_of_det_ne_zero 📖	mathematical	—	SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass separatingLeft_iff_det_ne_zero
separatingLeft_toLinearMap₂'_iff_det_ne_zero 📖	mathematical	—	SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module Algebra.to_smulCommClass Algebra.id instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂'	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass instSMulCommClass Matrix.exists_vecMul_eq_zero_iff Matrix.toLinearMap₂'_apply' Matrix.dotProduct_mulVec zero_dotProduct nondegenerate_toLinearMap₂'_iff_det_ne_zero
separatingLeft_toLinearMap₂'_of_det_ne_zero' 📖	mathematical	—	SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module Algebra.to_smulCommClass Algebra.id instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂'	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass instSMulCommClass separatingLeft_toLinearMap₂'_iff_det_ne_zero
separatingLeft_toMatrix₂'_iff 📖	mathematical	—	Matrix.SeparatingLeft Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' SeparatingLeft	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids instSMulCommClass smulCommClass_self Matrix.separatingLeft_toLinearMap₂'_iff Matrix.toLinearMap₂'_toMatrix'
separatingLeft_toMatrix₂_iff 📖	mathematical	—	Matrix.SeparatingLeft Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ SeparatingLeft	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids smulCommClass_self instSMulCommClass Matrix.separatingLeft_toLinearMap₂_iff Matrix.toLinearMap₂_toMatrix₂
separatingRight_iff_det_ne_zero 📖	mathematical	—	SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass Finite.of_fintype Matrix.separatingRight_iff_det_ne_zero separatingRight_toMatrix₂_iff
separatingRight_of_det_ne_zero 📖	mathematical	—	SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass separatingRight_iff_det_ne_zero
separatingRight_toLinearMap₂'_iff_det_ne_zero 📖	mathematical	—	SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module Algebra.to_smulCommClass Algebra.id instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂'	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass instSMulCommClass Matrix.exists_mulVec_eq_zero_iff Matrix.toLinearMap₂'_apply' dotProduct_zero nondegenerate_toLinearMap₂'_iff_det_ne_zero
separatingRight_toLinearMap₂'_of_det_ne_zero' 📖	mathematical	—	SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module Algebra.to_smulCommClass Algebra.id instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂'	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass instSMulCommClass separatingRight_toLinearMap₂'_iff_det_ne_zero
separatingRight_toMatrix₂'_iff 📖	mathematical	—	Matrix.SeparatingRight Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' SeparatingRight	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids instSMulCommClass smulCommClass_self Matrix.separatingRight_toLinearMap₂'_iff Matrix.toLinearMap₂'_toMatrix'
separatingRight_toMatrix₂_iff 📖	mathematical	—	Matrix.SeparatingRight Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ SeparatingRight	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids smulCommClass_self instSMulCommClass Matrix.separatingRight_toLinearMap₂_iff Matrix.toLinearMap₂_toMatrix₂
toLinearMap₂'Aux_toMatrix₂Aux 📖	mathematical	—	Matrix.toLinearMap₂'Aux DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid module Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module instFunLike toMatrix₂Aux Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ext_basis Finite.of_fintype instSMulCommClass Pi.basisFun_apply Matrix.toLinearMap₂'Aux_single
toMatrix'_toLinearMap₂' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid module Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' Matrix.toLinearMap₂'	—	LinearEquiv.apply_symm_apply instSMulCommClass RingHomInvPair.ids
toMatrix'_toLinearMapₛₗ₂' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid module Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrixₛₗ₂' Matrix.toLinearMapₛₗ₂'	—	LinearEquiv.apply_symm_apply instSMulCommClass RingHomInvPair.ids
toMatrix₂'_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid module Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' instFunLike Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids instSMulCommClass
toMatrix₂'_comp 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' comp RingHomCompTriple.ids Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction toMatrix'	—	Algebra.to_smulCommClass RingHomInvPair.ids instSMulCommClass RingHomCompTriple.ids Function.smulCommClass compl₂_id compl₁₂.eq_1 toMatrix₂'_compl₁₂ toMatrix'_id Matrix.mul_one
toMatrix₂'_compl₁₂ 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' compl₁₂ Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction toMatrix'	—	Algebra.to_smulCommClass Matrix.ext RingHomInvPair.ids instSMulCommClass Function.smulCommClass Finset.sum_congr Finset.sum_mul Finset.sum_comm Finite.of_fintype smulCommClass_self sum_repr_mul_repr_mul Finsupp.sum_fintype Pi.basisFun_apply MulZeroClass.zero_mul Finsupp.sum_fun_zero zero_smul smul_zero Pi.basisFun_repr mul_comm mul_left_comm mul_assoc
toMatrix₂'_compl₂ 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' compl₂ RingHomCompTriple.ids Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction toMatrix'	—	Algebra.to_smulCommClass RingHomInvPair.ids instSMulCommClass RingHomCompTriple.ids Function.smulCommClass comp_id compl₁₂.eq_1 toMatrix₂'_compl₁₂ toMatrix'_id Matrix.transpose_one Matrix.one_mul
toMatrix₂'_mul 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Pi.addCommMonoid Pi.Function.module Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂' compl₂ RingHomCompTriple.ids Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction Matrix.toLin'	—	Algebra.to_smulCommClass RingHomInvPair.ids instSMulCommClass RingHomCompTriple.ids Function.smulCommClass toMatrix₂'_compl₂ toMatrix'_toLin'
toMatrix₂Aux_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid module Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module instFunLike toMatrix₂Aux	—	instSMulCommClass
toMatrix₂Aux_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module instFunLike toMatrix₂Aux Module.Basis Module.Basis.instFunLike LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂	—	smulCommClass_self Matrix.ext instSMulCommClass RingHomInvPair.ids toMatrix₂_apply toMatrix₂Aux_apply
toMatrix₂_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ instFunLike Module.Basis Module.Basis.instFunLike	—	smulCommClass_self RingHomInvPair.ids instSMulCommClass Finite.of_fintype Module.Basis.equivFun_symm_apply Finset.sum_congr Pi.single_apply ite_smul one_smul zero_smul Finset.sum_ite_eq'
toMatrix₂_basisFun 📖	mathematical	—	toMatrix₂ Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule RingHom.id Pi.basisFun Finite.of_fintype toMatrix₂' smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	LinearEquiv.ext smulCommClass_self instSMulCommClass RingHomInvPair.ids Finite.of_fintype Matrix.ext toMatrix₂_apply toMatrix₂'_apply Pi.basisFun_apply
toMatrix₂_comp 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ comp Algebra.to_smulCommClass Algebra.id RingHomCompTriple.ids Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose toMatrix Finite.of_fintype	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass RingHomCompTriple.ids Finite.of_fintype compl₂_id compl₁₂.eq_1 toMatrix₂_compl₁₂ toMatrix_id_eq_basis_toMatrix Module.Basis.toMatrix_self Matrix.mul_one
toMatrix₂_compl₁₂ 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ compl₁₂ Algebra.to_smulCommClass Algebra.id Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose toMatrix Finite.of_fintype	—	Algebra.to_smulCommClass Matrix.ext RingHomInvPair.ids smulCommClass_self instSMulCommClass Finite.of_fintype toMatrix₂_apply Finset.sum_congr toMatrix_apply Finset.sum_mul Finset.sum_comm sum_repr_mul_repr_mul Finsupp.sum_fintype MulZeroClass.zero_mul Finsupp.sum_fun_zero zero_smul smul_zero mul_comm mul_left_comm mul_assoc
toMatrix₂_compl₂ 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ compl₂ RingHomCompTriple.ids Algebra.to_smulCommClass Algebra.id Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib toMatrix Finite.of_fintype	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass RingHomCompTriple.ids Finite.of_fintype comp_id compl₁₂.eq_1 toMatrix₂_compl₁₂ toMatrix_id_eq_basis_toMatrix Module.Basis.toMatrix_self Matrix.transpose_one Matrix.one_mul
toMatrix₂_mul 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ compl₂ RingHomCompTriple.ids Algebra.to_smulCommClass Algebra.id Matrix.toLin Finite.of_fintype	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass RingHomCompTriple.ids Finite.of_fintype toMatrix₂_compl₂ toMatrix_toLin
toMatrix₂_mul_basis_toMatrix 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.transpose Module.Basis.toMatrix DFunLike.coe Module.Basis Module.Basis.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass Finite.of_fintype toMatrix₂_compl₁₂ compl₁₂_id_id
toMatrix₂_symm 📖	mathematical	—	LinearEquiv.symm LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module RingHomInvPair.ids toMatrix₂ Matrix.toLinearMap₂	—	RingHomInvPair.ids smulCommClass_self instSMulCommClass
toMatrix₂_symm' 📖	mathematical	—	LinearEquiv.symm LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module RingHomInvPair.ids toMatrix₂ Matrix.toLinearMapₛₗ₂	—	RingHomInvPair.ids smulCommClass_self instSMulCommClass
toMatrix₂_toLinearMap₂ 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ Matrix.toLinearMap₂	—	LinearEquiv.apply_symm_apply smulCommClass_self instSMulCommClass RingHomInvPair.ids
toMatrix₂_toLinearMapₛₗ₂ 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂ Matrix.toLinearMapₛₗ₂	—	LinearEquiv.apply_symm_apply smulCommClass_self instSMulCommClass RingHomInvPair.ids
toMatrixₛₗ₂'_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid module Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrixₛₗ₂' instFunLike Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids instSMulCommClass
toMatrixₛₗ₂'_symm 📖	mathematical	—	LinearEquiv.symm LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid module Matrix CommSemiring.toSemiring Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module RingHom.id RingHomInvPair.ids toMatrixₛₗ₂' Matrix.toLinearMapₛₗ₂'	—	RingHomInvPair.ids instSMulCommClass

LinearMap.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMatrix₂ 📖	mathematical	LinearMap.Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring	Matrix.Nondegenerate Finite.of_fintype DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix₂	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass LinearMap.nondegenerate_toMatrix₂_iff
toMatrix₂' 📖	mathematical	LinearMap.Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid Pi.Function.module RingHom.id Semiring.toNonAssocSemiring	Matrix.Nondegenerate Finite.of_fintype DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id Matrix Matrix.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix₂'	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids LinearMap.instSMulCommClass LinearMap.nondegenerate_toMatrix₂'_iff

LinearMap.SeparatingLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMatrix₂ 📖	mathematical	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring	Matrix.SeparatingLeft Finite.of_fintype DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix₂	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass LinearMap.separatingLeft_toMatrix₂_iff
toMatrix₂' 📖	mathematical	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid Pi.Function.module RingHom.id Semiring.toNonAssocSemiring	Matrix.SeparatingLeft Finite.of_fintype DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id Matrix Matrix.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix₂'	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids LinearMap.instSMulCommClass LinearMap.separatingLeft_toMatrix₂'_iff

LinearMap.SeparatingRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMatrix₂ 📖	mathematical	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring	Matrix.SeparatingRight Finite.of_fintype DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix₂	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass LinearMap.separatingRight_toMatrix₂_iff
toMatrix₂' 📖	mathematical	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid Pi.Function.module RingHom.id Semiring.toNonAssocSemiring	Matrix.SeparatingRight Finite.of_fintype DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id Matrix Matrix.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix₂'	—	Algebra.to_smulCommClass Finite.of_fintype RingHomInvPair.ids LinearMap.instSMulCommClass LinearMap.separatingRight_toMatrix₂'_iff

Matrix

Definitions

Name	Category	Theorems
IsAdjointPair 📖	MathDef	6 math math: mem_pairSelfAdjointMatricesSubmodule, isAdjointPair_toLinearMap₂, mem_pairSelfAdjointMatricesSubmodule', isAdjointPair_equiv', isAdjointPair_toLinearMap₂', isAdjointPair_equiv
IsSelfAdjoint 📖	MathDef	2 math math: mem_selfAdjointMatricesSubmodule, mem_selfAdjointMatricesSubmodule'
IsSkewAdjoint 📖	MathDef	2 math math: mem_skewAdjointMatricesSubmodule', mem_skewAdjointMatricesSubmodule
toLinearMap₂ 📖	CompOp	18 math math: SeparatingRight.toLinearMap₂, separatingRight_toLinearMap₂_iff, toLinearMap₂_toMatrix₂, Nondegenerate.toLinearMap₂, isAdjointPair_toLinearMap₂, toLinearMap₂_compl₁₂, LinearMap.toMatrix₂_toLinearMap₂, LinearMap.toMatrix₂_symm, toLinearMap₂_symm, nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂, nondegenerate_toLinearMap₂_iff, toLinearMap₂_basisFun, toLinearMap₂_apply, separatingLeft_toLinearMap₂_iff, toLinearMap₂_apply_basis, separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂, SeparatingLeft.toLinearMap₂, separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂
toLinearMap₂' 📖	CompOp	27 math math: SimpleGraph.lapMatrix_toLinearMap₂', separatingRight_toLinearMap₂'_iff, toLinearMap₂'_comp, LinearMap.nondegenerate_toLinearMap₂'_of_det_ne_zero', SeparatingLeft.toLinearMap₂', toLinearMap₂'_apply', SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, toLinearMap₂'_apply, SeparatingRight.toLinearMap₂', PosSemidef.toLinearMap₂'_zero_iff, toLinearMap₂'_toMatrix', isAdjointPair_toLinearMap₂', LinearMap.toMatrix'_toLinearMap₂', nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂, toLinearMap₂_basisFun, LinearMap.nondegenerate_toLinearMap₂'_iff_det_ne_zero, toLinearMap₂'_single, LinearMap.separatingRight_toLinearMap₂'_of_det_ne_zero', separatingLeft_toLinearMap₂'_iff, LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero', nondegenerate_toLinearMap₂'_iff, LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero, separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂, LinearMap.separatingRight_toLinearMap₂'_iff_det_ne_zero, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj, Nondegenerate.toLinearMap₂', separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂
toLinearMap₂'Aux 📖	CompOp	4 math math: toLinearMap₂'Aux_single, toLinearMapₛₗ₂'_aux_eq, toMatrix₂Aux_toLinearMap₂'Aux, LinearMap.toLinearMap₂'Aux_toMatrix₂Aux
toLinearMapₛₗ₂ 📖	CompOp	6 math math: LinearMap.toMatrix₂_toLinearMapₛₗ₂, toLinearMapₛₗ₂_apply, toLinearMapₛₗ₂_symm, toLinearMapₛₗ₂_apply_basis, LinearMap.toMatrix₂_symm', toLinearMapₛₗ₂_toMatrix₂
toLinearMapₛₗ₂' 📖	CompOp	7 math math: LinearMap.toMatrixₛₗ₂'_symm, toLinearMapₛₗ₂'_single, toLinearMapₛₗ₂'_symm, toLinearMapₛₗ₂'_aux_eq, toLinearMapₛₗ₂'_toMatrix', toLinearMapₛₗ₂'_apply, LinearMap.toMatrix'_toLinearMapₛₗ₂'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAdjointPair_equiv 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	IsAdjointPair instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid transpose inv	—	isUnit_iff_isUnit_det isUnit_det_transpose Units.eq_mul_inv_iff_mul_eq mul_assoc Units.inv_mul_eq_iff_eq_mul transpose_mul transpose_nonsing_inv
nondegenerate_toLinearMap₂'_iff 📖	mathematical	—	LinearMap.Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' Nondegenerate Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass LinearMap.instSMulCommClass Finite.of_fintype separatingLeft_toLinearMap₂'_iff separatingRight_toLinearMap₂'_iff Nondegenerate.separatingLeft Nondegenerate.separatingRight
nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂ 📖	mathematical	—	LinearMap.Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' toLinearMap₂	—	RingHomInvPair.ids smulCommClass_self RingHomCompTriple.ids Finite.of_fintype Algebra.to_smulCommClass LinearMap.instSMulCommClass LinearMap.nondegenerate_congr_iff
nondegenerate_toLinearMap₂_iff 📖	mathematical	—	LinearMap.Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂ Nondegenerate Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Finite.of_fintype Algebra.to_smulCommClass nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂ nondegenerate_toLinearMap₂'_iff
separatingLeft_toLinearMap₂'_iff 📖	mathematical	—	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' SeparatingLeft Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass LinearMap.instSMulCommClass Finite.of_fintype separatingLeft_def toLinearMap₂'_apply' SeparatingLeft.toLinearMap₂'
separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂ 📖	mathematical	—	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' toLinearMap₂	—	RingHomInvPair.ids smulCommClass_self RingHomCompTriple.ids Finite.of_fintype Algebra.to_smulCommClass LinearMap.instSMulCommClass LinearMap.separatingLeft_congr_iff
separatingLeft_toLinearMap₂_iff 📖	mathematical	—	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂ SeparatingLeft Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Finite.of_fintype Algebra.to_smulCommClass separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂ separatingLeft_toLinearMap₂'_iff
separatingRight_toLinearMap₂'_iff 📖	mathematical	—	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' SeparatingRight Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass LinearMap.instSMulCommClass Finite.of_fintype separatingRight_def toLinearMap₂'_apply' SeparatingRight.toLinearMap₂'
separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂ 📖	mathematical	—	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' toLinearMap₂	—	RingHomInvPair.ids smulCommClass_self RingHomCompTriple.ids Finite.of_fintype Algebra.to_smulCommClass LinearMap.instSMulCommClass LinearMap.separatingRight_congr_iff
separatingRight_toLinearMap₂_iff 📖	mathematical	—	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂ SeparatingRight Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Finite.of_fintype Algebra.to_smulCommClass separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂ separatingRight_toLinearMap₂'_iff
toLinearMap₂'Aux_single 📖	mathematical	—	DFunLike.coe LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module toLinearMap₂'Aux Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toLinearMap₂'Aux.eq_1 LinearMap.mk₂'ₛₗ_apply Finset.sum_congr ite_smul one_smul zero_smul Finset.sum_ite_eq smul_ite smul_zero Pi.single_eq_of_ne' map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Pi.single_eq_same map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
toLinearMap₂'_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module LinearEquiv CommSemiring.toSemiring RingHomInvPair.ids Matrix addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass	—	Finset.sum_congr RingHom.id_apply SMulCommClass.smul_comm
toLinearMap₂'_apply' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearEquiv RingHomInvPair.ids Matrix addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib mulVec	—	Algebra.to_smulCommClass RingHomInvPair.ids LinearMap.instSMulCommClass toLinearMap₂'_apply Finset.sum_congr Finset.mul_sum smul_eq_mul mul_comm mul_assoc
toLinearMap₂'_comp 📖	mathematical	—	LinearMap.compl₁₂ CommSemiring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Algebra.to_smulCommClass Algebra.id DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction toLin' instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib transpose	—	LinearEquiv.injective Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomInvPair.ids Function.smulCommClass LinearMap.toMatrix₂'_compl₁₂ LinearMap.toMatrix'_toLin' LinearMap.toMatrix'_toLinearMap₂'
toLinearMap₂'_single 📖	mathematical	—	DFunLike.coe LinearMap Nat.instSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule AddCommMonoid.toNatModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module AddMonoid.nat_smulCommClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul Nat.instMonoid Module.toDistribMulAction LinearEquiv CommSemiring.toSemiring RingHomInvPair.ids Matrix addCommMonoid module MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instSMulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' Pi.single MulZeroClass.toZero Nat.instMulZeroClass	—	toLinearMap₂'Aux_single AddMonoid.nat_smulCommClass
toLinearMap₂'_toMatrix' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap.module addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂' LinearMap.toMatrix₂'	—	LinearEquiv.apply_symm_apply LinearMap.instSMulCommClass RingHomInvPair.ids
toLinearMap₂_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearEquiv RingHomInvPair.ids Matrix addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂ Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Module.Basis.repr	—	Finset.sum_congr Finite.of_fintype RingHomInvPair.ids smul_algebra_smul_comm IsScalarTower.left
toLinearMap₂_apply_basis 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearEquiv RingHomInvPair.ids Matrix addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂ Module.Basis Module.Basis.instFunLike	—	toLinearMapₛₗ₂_apply_basis
toLinearMap₂_basisFun 📖	mathematical	—	toLinearMap₂ Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule Pi.basisFun Finite.of_fintype toLinearMap₂' smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	LinearEquiv.ext smulCommClass_self LinearMap.instSMulCommClass RingHomInvPair.ids Finite.of_fintype LinearMap.pi_ext' LinearMap.ext_ring RingHomCompTriple.ids toLinearMap₂_apply Finset.sum_congr Pi.basisFun_repr toLinearMap₂'_apply
toLinearMap₂_compl₁₂ 📖	mathematical	—	LinearMap.compl₁₂ CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂ toLin Finite.of_fintype instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib transpose	—	LinearEquiv.injective smulCommClass_self LinearMap.instSMulCommClass RingHomInvPair.ids Finite.of_fintype Algebra.to_smulCommClass LinearMap.toMatrix₂_compl₁₂ LinearMap.toMatrix_toLin LinearMap.toMatrix₂_toLinearMap₂
toLinearMap₂_symm 📖	mathematical	—	LinearEquiv.symm Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHomInvPair.ids toLinearMap₂ LinearMap.toMatrix₂	—	LinearEquiv.symm_symm smulCommClass_self LinearMap.instSMulCommClass RingHomInvPair.ids
toLinearMap₂_toMatrix₂ 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMap₂ LinearMap.toMatrix₂	—	smulCommClass_self LinearEquiv.apply_symm_apply LinearMap.instSMulCommClass RingHomInvPair.ids
toLinearMapₛₗ₂'_apply 📖	mathematical	—	DFunLike.coe LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module LinearEquiv CommSemiring.toSemiring RingHom.id RingHomInvPair.ids Matrix addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapₛₗ₂' Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass RingHom RingHom.instFunLike	—	RingHomInvPair.ids LinearMap.instSMulCommClass toLinearMapₛₗ₂'.eq_1 LinearMap.toLinearMap₂'Aux_toMatrix₂Aux toMatrix₂Aux_toLinearMap₂'Aux LinearMap.toMatrixₛₗ₂'.eq_1 toLinearMap₂'Aux.eq_1 LinearMap.mk₂'ₛₗ_apply Finset.sum_congr SMulCommClass.smul_comm
toLinearMapₛₗ₂'_aux_eq 📖	mathematical	—	toLinearMap₂'Aux DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap.module addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapₛₗ₂'	—	—
toLinearMapₛₗ₂'_single 📖	mathematical	—	DFunLike.coe LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module LinearEquiv CommSemiring.toSemiring RingHom.id RingHomInvPair.ids Matrix addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapₛₗ₂' Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toLinearMap₂'Aux_single
toLinearMapₛₗ₂'_symm 📖	mathematical	—	LinearEquiv.symm Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap.module CommSemiring.toSemiring addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id RingHomInvPair.ids toLinearMapₛₗ₂' LinearMap.toMatrixₛₗ₂'	—	LinearEquiv.symm_symm LinearMap.instSMulCommClass RingHomInvPair.ids
toLinearMapₛₗ₂'_toMatrix' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap.module addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapₛₗ₂' LinearMap.toMatrixₛₗ₂'	—	LinearEquiv.apply_symm_apply LinearMap.instSMulCommClass RingHomInvPair.ids
toLinearMapₛₗ₂_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearEquiv RingHomInvPair.ids Matrix addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapₛₗ₂ Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass RingHom RingHom.instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Module.Basis.repr	—	Finset.sum_congr Finite.of_fintype RingHomInvPair.ids smul_algebra_smul_comm IsScalarTower.left
toLinearMapₛₗ₂_apply_basis 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearEquiv RingHomInvPair.ids Matrix addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapₛₗ₂ Module.Basis Module.Basis.instFunLike	—	smulCommClass_self RingHomInvPair.ids LinearMap.instSMulCommClass toLinearMapₛₗ₂_apply Finset.sum_congr Module.Basis.repr_self Finset.sum_eq_single_of_mem Finsupp.single_eq_of_ne map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_smul Finset.sum_const_zero Finsupp.single_eq_same map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass smul_zero one_smul
toLinearMapₛₗ₂_symm 📖	mathematical	—	LinearEquiv.symm Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHomInvPair.ids toLinearMapₛₗ₂ LinearMap.toMatrix₂	—	LinearEquiv.symm_symm smulCommClass_self LinearMap.instSMulCommClass RingHomInvPair.ids
toLinearMapₛₗ₂_toMatrix₂ 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapₛₗ₂ LinearMap.toMatrix₂	—	smulCommClass_self LinearEquiv.apply_symm_apply LinearMap.instSMulCommClass RingHomInvPair.ids
toMatrix₂Aux_toLinearMap₂'Aux 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap.module Matrix addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction module LinearMap.instFunLike LinearMap.toMatrix₂Aux Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne toLinearMap₂'Aux	—	ext LinearMap.instSMulCommClass toLinearMap₂'Aux_single

Matrix.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLinearMap₂ 📖	mathematical	Matrix.Nondegenerate Finite.of_fintype	LinearMap.Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂	—	Finite.of_fintype RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Matrix.nondegenerate_toLinearMap₂_iff
toLinearMap₂' 📖	mathematical	Matrix.Nondegenerate Finite.of_fintype	LinearMap.Nondegenerate CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂'	—	Finite.of_fintype RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass LinearMap.instSMulCommClass Matrix.SeparatingLeft.toLinearMap₂' separatingLeft Matrix.SeparatingRight.toLinearMap₂' separatingRight

Matrix.SeparatingLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLinearMap₂ 📖	mathematical	Matrix.SeparatingLeft Finite.of_fintype	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂	—	Finite.of_fintype RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Matrix.separatingLeft_toLinearMap₂_iff
toLinearMap₂' 📖	mathematical	Matrix.SeparatingLeft Finite.of_fintype	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂'	—	Finite.of_fintype RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass LinearMap.instSMulCommClass Matrix.toLinearMap₂'_apply'

Matrix.SeparatingRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLinearMap₂ 📖	mathematical	Matrix.SeparatingRight Finite.of_fintype	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂	—	Finite.of_fintype RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Matrix.separatingRight_toLinearMap₂_iff
toLinearMap₂' 📖	mathematical	Matrix.SeparatingRight Finite.of_fintype	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂'	—	Finite.of_fintype RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass LinearMap.instSMulCommClass Matrix.toLinearMap₂'_apply'

(root)

Definitions

Name	Category	Theorems
pairSelfAdjointMatricesSubmodule 📖	CompOp	2 math math: mem_pairSelfAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule'
selfAdjointMatricesSubmodule 📖	CompOp	2 math math: mem_selfAdjointMatricesSubmodule, mem_selfAdjointMatricesSubmodule'
skewAdjointMatricesSubmodule 📖	CompOp	3 math math: mem_skewAdjointMatricesSubmodule', mem_skewAdjointMatricesLieSubalgebra, mem_skewAdjointMatricesSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_dotProduct_toMatrix₂_mulVec 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Matrix.mulVec smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module LinearMap.toMatrix₂	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Module.Basis.sum_repr Finset.sum_congr mul_comm Finset.sum_comm map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.map_smulₛₗ LinearMap.coe_sum Finset.sum_apply Finset.mul_sum Matrix.mulVec_eq_sum IsCentralScalar.op_smul_eq_smul Pi.isCentralScalar CommSemigroup.isCentralScalar LinearMap.toMatrix₂_apply
dotProduct_toMatrix₂_mulVec 📖	mathematical	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe RingHom RingHom.instFunLike Matrix.mulVec LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Semiring.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix₂ LinearMap.instFunLike Algebra.to_smulCommClass Algebra.id Pi.addCommMonoid Pi.Function.module LinearEquiv.symm Module.Basis.equivFun Finite.of_fintype	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Finite.of_fintype Finset.sum_congr Matrix.mulVec_eq_sum IsCentralScalar.op_smul_eq_smul Pi.isCentralScalar CommSemigroup.isCentralScalar Finset.sum_apply LinearMap.toMatrix₂_apply Finset.mul_sum Module.Basis.equivFun_symm_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass LinearMap.coe_sum Finset.sum_comm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
isAdjointPair_toLinearMap₂ 📖	mathematical	—	LinearMap.IsAdjointPair CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂ LinearMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Matrix.toLin Finite.of_fintype Matrix.IsAdjointPair	—	RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Finite.of_fintype RingHomCompTriple.ids LinearMap.isAdjointPair_iff_comp_eq_compl₂ Algebra.to_smulCommClass LinearEquiv.injective LinearMap.toMatrix₂_comp LinearMap.toMatrix₂_compl₂ LinearMap.toMatrix_toLin LinearMap.toMatrix₂_toLinearMap₂
isAdjointPair_toLinearMap₂' 📖	mathematical	—	LinearMap.IsAdjointPair CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.addCommMonoid Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂' LinearMap.instFunLike Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Matrix.toLin' Matrix.IsAdjointPair	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass LinearMap.instSMulCommClass Function.smulCommClass RingHomCompTriple.ids LinearMap.isAdjointPair_iff_comp_eq_compl₂ LinearEquiv.injective LinearMap.toMatrix₂'_comp LinearMap.toMatrix₂'_compl₂ LinearMap.toMatrix'_toLin' LinearMap.toMatrix'_toLinearMap₂'
mem_pairSelfAdjointMatricesSubmodule 📖	mathematical	—	Matrix Submodule CommSemiring.toSemiring CommRing.toCommSemiring Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.module Semiring.toModule SetLike.instMembership Submodule.setLike pairSelfAdjointMatricesSubmodule Matrix.IsAdjointPair	—	RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomSurjective.invPair
mem_selfAdjointMatricesSubmodule 📖	mathematical	—	Matrix Submodule CommSemiring.toSemiring CommRing.toCommSemiring Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.module Semiring.toModule SetLike.instMembership Submodule.setLike selfAdjointMatricesSubmodule Matrix.IsSelfAdjoint	—	selfAdjointMatricesSubmodule.eq_1 mem_pairSelfAdjointMatricesSubmodule Matrix.IsSelfAdjoint.eq_1
mem_skewAdjointMatricesSubmodule 📖	mathematical	—	Matrix Submodule CommSemiring.toSemiring CommRing.toCommSemiring Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.module Semiring.toModule SetLike.instMembership Submodule.setLike skewAdjointMatricesSubmodule Matrix.IsSkewAdjoint	—	skewAdjointMatricesSubmodule.eq_1 mem_pairSelfAdjointMatricesSubmodule neg_mul mul_neg

---

← Back to Index