BilinearForm

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

Statistics

Metric	Count
Definitions toMatrix, toMatrixAux, toMatrix, toMatrix', toMatrixAux, toBilin, toBilin', toBilin'Aux, selfAdjointMatricesSubmodule', skewAdjointMatricesSubmodule'	10
Theorems apply_eq_dotProduct_toMatrix_mulVec, dotProduct_toMatrix_mulVec, mul_toMatrix, mul_toMatrix_mul, toMatrix_apply, toMatrix_basisFun, toMatrix_comp, toMatrix_compLeft, toMatrix_compRight, toMatrix_mul, toMatrix_mul_basis_toMatrix, toMatrix_symm, toMatrix_toBilin, toMatrixAux_eq, ofSeparatingLeft, ofSeparatingRight, toMatrix, toMatrix', toMatrix, toMatrix', toMatrix, toMatrix', apply_eq_dotProduct_toMatrix_mulVec, dotProduct_toMatrix_mulVec, mul_toMatrix, mul_toMatrix', mul_toMatrix'_mul, mul_toMatrix_mul, nondegenerate_iff_det_ne_zero, nondegenerate_iff_ker_eq_bot, nondegenerate_of_det_ne_zero, nondegenerate_toBilin'_iff_det_ne_zero, nondegenerate_toBilin'_of_det_ne_zero', nondegenerate_toMatrix'_iff, nondegenerate_toMatrix_iff, separatingLeft_toMatrix'_iff, separatingLeft_toMatrix_iff, separatingRight_toMatrix'_iff, separatingRight_toMatrix_iff, toMatrix'_apply, toMatrix'_comp, toMatrix'_compLeft, toMatrix'_compRight, toMatrix'_mul, toMatrix'_symm, toMatrix'_toBilin', toMatrixAux_apply, toMatrixAux_eq, toMatrix_apply, toMatrix_basisFun, toMatrix_comp, toMatrix_compLeft, toMatrix_compRight, toMatrix_mul, toMatrix_mul_basis_toMatrix, toMatrix_symm, toMatrix_toBilin, toBilin'Aux_toMatrixAux, toBilin, toBilin', toBilin, toBilin', toBilin, toBilin', isAdjointPair_equiv', nondegenerate_toBilin'_iff, nondegenerate_toBilin'_iff_nondegenerate_toBilin, nondegenerate_toBilin_iff, separatingLeft_toBilin'_iff, separatingLeft_toBilin_iff, separatingRight_toBilin'_iff, separatingRight_toBilin_iff, toBilin'Aux_eq, toBilin'Aux_single, toBilin'_apply, toBilin'_apply', toBilin'_comp, toBilin'_single, toBilin'_symm, toBilin'_toMatrix', toBilin_apply, toBilin_basisFun, toBilin_comp, toBilin_symm, toBilin_toMatrix, mem_pairSelfAdjointMatricesSubmodule', mem_selfAdjointMatricesSubmodule', mem_skewAdjointMatricesSubmodule', toBilin'Aux_toMatrixAux	89
Total	99

BilinForm

Definitions

Name	Category	Theorems
toMatrix 📖	CompOp	—
toMatrixAux 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_dotProduct_toMatrix_mulVec 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Matrix.mulVec Matrix Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module LinearMap.BilinForm.toMatrix	—	LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec
dotProduct_toMatrix_mulVec 📖	mathematical	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.mulVec DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix LinearMap.instFunLike Pi.addCommMonoid Pi.Function.module LinearEquiv.symm Module.Basis.equivFun Finite.of_fintype	—	LinearMap.BilinForm.dotProduct_toMatrix_mulVec
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.BilinForm LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix LinearMap.BilinForm.compLeft smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Matrix.toLin Finite.of_fintype Matrix.transpose	—	LinearMap.BilinForm.mul_toMatrix
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.BilinForm LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix LinearMap.BilinForm.comp smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Matrix.toLin Finite.of_fintype Matrix.transpose	—	LinearMap.BilinForm.mul_toMatrix_mul
toMatrix_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix LinearMap.instFunLike Module.Basis Module.Basis.instFunLike	—	LinearMap.BilinForm.toMatrix_apply
toMatrix_basisFun 📖	mathematical	—	LinearMap.BilinForm.toMatrix Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule Pi.basisFun Finite.of_fintype LinearMap.BilinForm.toMatrix'	—	LinearMap.BilinForm.toMatrix_basisFun
toMatrix_comp 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix LinearMap.BilinForm.comp Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.toMatrix Finite.of_fintype	—	LinearMap.BilinForm.toMatrix_comp
toMatrix_compLeft 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix LinearMap.BilinForm.compLeft Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.toMatrix Finite.of_fintype	—	LinearMap.BilinForm.toMatrix_compLeft
toMatrix_compRight 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix LinearMap.BilinForm.compRight Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.toMatrix Finite.of_fintype	—	LinearMap.BilinForm.toMatrix_compRight
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.BilinForm LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix LinearMap.BilinForm.compRight smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Matrix.toLin Finite.of_fintype	—	LinearMap.BilinForm.toMatrix_mul
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.BilinForm LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix	—	LinearMap.BilinForm.toMatrix_mul_basis_toMatrix
toMatrix_symm 📖	mathematical	—	LinearEquiv.symm LinearMap.BilinForm Matrix CommSemiring.toSemiring LinearMap.addCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module RingHomInvPair.ids LinearMap.BilinForm.toMatrix Matrix.toBilin	—	LinearMap.BilinForm.toMatrix_symm
toMatrix_toBilin 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix Matrix.toBilin	—	LinearMap.BilinForm.toMatrix_toBilin

BilinearForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMatrixAux_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.BilinForm Matrix LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module LinearMap.instFunLike LinearMap.BilinForm.toMatrixAux Module.Basis Module.Basis.instFunLike LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix	—	LinearMap.BilinForm.toMatrixAux_eq

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toBilin'Aux_toMatrixAux 📖	mathematical	—	Matrix.toBilin'Aux DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module instFunLike BilinForm.toMatrixAux Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Algebra.to_smulCommClass instSMulCommClass BilinForm.toMatrixAux.eq_1 Matrix.toBilin'Aux.eq_1 toLinearMap₂'Aux_toMatrix₂Aux

LinearMap.BilinForm

Definitions

Name	Category	Theorems
toMatrix 📖	CompOp	40 math math: toMatrix_toBilin, BilinForm.toMatrix_symm, toMatrixAux_eq, toMatrix_basisFun, toMatrix_compRight, SeparatingRight.toMatrix, Matrix.toBilin_symm, nondegenerate_toMatrix_iff, apply_eq_dotProduct_toMatrix_mulVec, BilinForm.mul_toMatrix_mul, Algebra.traceForm_toMatrix, BilinForm.dotProduct_toMatrix_mulVec, toMatrix_apply, BilinForm.toMatrix_toBilin, dotProduct_toMatrix_mulVec, BilinForm.toMatrix_comp, BilinearForm.toMatrixAux_eq, separatingRight_toMatrix_iff, toMatrix_symm, SeparatingLeft.toMatrix, BilinForm.toMatrix_compRight, BilinForm.toMatrix_mul_basis_toMatrix, Algebra.traceMatrix_of_basis, Matrix.toBilin_toMatrix, mul_toMatrix_mul, toMatrix_mul_basis_toMatrix, toMatrix_mul, toMatrix_compLeft, BilinForm.toMatrix_apply, mul_toMatrix, BilinForm.toMatrix_mul, BilinForm.toMatrix_basisFun, BilinForm.mul_toMatrix, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, BilinForm.toMatrix_compLeft, toMatrix_comp, Nondegenerate.toMatrix, Algebra.traceForm_toMatrix_powerBasis, separatingLeft_toMatrix_iff
toMatrix' 📖	CompOp	19 math math: toMatrix_basisFun, toMatrix'_symm, toMatrix'_apply, separatingLeft_toMatrix'_iff, mul_toMatrix'_mul, separatingRight_toMatrix'_iff, Matrix.toBilin'_symm, toMatrix'_compLeft, SeparatingLeft.toMatrix', nondegenerate_toMatrix'_iff, mul_toMatrix', toMatrix'_comp, BilinForm.toMatrix_basisFun, toMatrix'_mul, toMatrix'_toBilin', Nondegenerate.toMatrix', SeparatingRight.toMatrix', Matrix.toBilin'_toMatrix', toMatrix'_compRight
toMatrixAux 📖	CompOp	5 math math: toMatrixAux_eq, LinearMap.toBilin'Aux_toMatrixAux, toBilin'Aux_toMatrixAux, BilinearForm.toMatrixAux_eq, toMatrixAux_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_dotProduct_toMatrix_mulVec 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Matrix.mulVec Matrix Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module toMatrix	—	apply_eq_dotProduct_toMatrix₂_mulVec
dotProduct_toMatrix_mulVec 📖	mathematical	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.mulVec DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix LinearMap.instFunLike Pi.addCommMonoid Pi.Function.module LinearEquiv.symm Module.Basis.equivFun Finite.of_fintype	—	dotProduct_toMatrix₂_mulVec
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.BilinForm LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix compLeft smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Matrix.toLin Finite.of_fintype Matrix.transpose	—	LinearMap.mul_toMatrix₂
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.BilinForm Pi.addCommMonoid Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' compLeft Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction Matrix.toLin' Matrix.transpose	—	LinearMap.mul_toMatrix'
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.BilinForm Pi.addCommMonoid Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' comp Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction Matrix.toLin' Matrix.transpose	—	LinearMap.mul_toMatrix₂'_mul
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.BilinForm LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix comp smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Matrix.toLin Finite.of_fintype Matrix.transpose	—	LinearMap.mul_toMatrix₂_mul
nondegenerate_iff_det_ne_zero 📖	mathematical	—	Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Finite.of_fintype Matrix.nondegenerate_iff_det_ne_zero nondegenerate_toMatrix_iff
nondegenerate_iff_ker_eq_bot 📖	mathematical	—	Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.ker LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module Bot.bot Submodule Submodule.instBot	—	Nondegenerate.ker_eq_bot Nondegenerate.ofSeparatingLeft smulCommClass_self LinearMap.separatingLeft_iff_ker_eq_bot
nondegenerate_of_det_ne_zero 📖	mathematical	—	Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass nondegenerate_iff_det_ne_zero
nondegenerate_toBilin'_iff_det_ne_zero 📖	mathematical	—	Nondegenerate CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap.BilinForm Matrix.addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toBilin'	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Finite.of_fintype Matrix.nondegenerate_toBilin'_iff Matrix.nondegenerate_iff_det_ne_zero
nondegenerate_toBilin'_of_det_ne_zero' 📖	mathematical	—	Nondegenerate CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap.BilinForm Matrix.addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toBilin'	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass nondegenerate_toBilin'_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.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' Nondegenerate NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	LinearMap.nondegenerate_toMatrix₂'_iff
nondegenerate_toMatrix_iff 📖	mathematical	—	Matrix.Nondegenerate Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm AddCommGroup.toAddCommMonoid Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Nondegenerate	—	Finite.of_fintype RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Matrix.nondegenerate_toBilin_iff Matrix.toBilin_toMatrix
separatingLeft_toMatrix'_iff 📖	mathematical	—	Matrix.SeparatingLeft Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' LinearMap.SeparatingLeft NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Finite.of_fintype RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Matrix.separatingLeft_toBilin'_iff Matrix.toBilin'_toMatrix'
separatingLeft_toMatrix_iff 📖	mathematical	—	Matrix.SeparatingLeft Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm AddCommGroup.toAddCommMonoid Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix LinearMap.SeparatingLeft	—	Finite.of_fintype RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Matrix.separatingLeft_toBilin_iff Matrix.toBilin_toMatrix
separatingRight_toMatrix'_iff 📖	mathematical	—	Matrix.SeparatingRight Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' LinearMap.SeparatingRight NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Finite.of_fintype RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Matrix.separatingRight_toBilin'_iff Matrix.toBilin'_toMatrix'
separatingRight_toMatrix_iff 📖	mathematical	—	Matrix.SeparatingRight Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm AddCommGroup.toAddCommMonoid Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix LinearMap.SeparatingRight	—	Finite.of_fintype RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Matrix.separatingRight_toBilin_iff Matrix.toBilin_toMatrix
toMatrix'_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' LinearMap.instFunLike Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	LinearMap.toMatrix₂'_apply
toMatrix'_comp 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' comp Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction LinearMap.toMatrix'	—	LinearMap.toMatrix₂'_compl₁₂
toMatrix'_compLeft 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' compLeft Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction LinearMap.toMatrix'	—	LinearMap.toMatrix₂'_comp
toMatrix'_compRight 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' compRight Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction LinearMap.toMatrix'	—	LinearMap.toMatrix₂'_compl₂
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.BilinForm Pi.addCommMonoid Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' compRight Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction Matrix.toLin'	—	LinearMap.toMatrix₂'_mul
toMatrix'_symm 📖	mathematical	—	LinearEquiv.symm LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid LinearMap RingHom.id LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module RingHomInvPair.ids toMatrix' Matrix.toBilin'	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass
toMatrix'_toBilin' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' Matrix.toBilin'	—	LinearEquiv.apply_symm_apply LinearMap.instSMulCommClass RingHomInvPair.ids
toMatrixAux_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.BilinForm Matrix LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module LinearMap.instFunLike toMatrixAux	—	LinearMap.toMatrix₂Aux_apply Algebra.to_smulCommClass
toMatrixAux_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.BilinForm Matrix LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module LinearMap.instFunLike toMatrixAux Module.Basis Module.Basis.instFunLike LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix	—	LinearMap.toMatrix₂Aux_eq
toMatrix_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix LinearMap.instFunLike Module.Basis Module.Basis.instFunLike	—	LinearMap.toMatrix₂_apply
toMatrix_basisFun 📖	mathematical	—	toMatrix Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule Pi.basisFun Finite.of_fintype toMatrix'	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Finite.of_fintype toMatrix.eq_1 toMatrix'.eq_1 smulCommClass_self LinearMap.toMatrix₂_basisFun
toMatrix_comp 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix comp Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.toMatrix Finite.of_fintype	—	LinearMap.toMatrix₂_compl₁₂
toMatrix_compLeft 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix compLeft Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.toMatrix Finite.of_fintype	—	LinearMap.toMatrix₂_comp
toMatrix_compRight 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix compRight Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.toMatrix Finite.of_fintype	—	LinearMap.toMatrix₂_compl₂
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.BilinForm LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix compRight smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Matrix.toLin Finite.of_fintype	—	LinearMap.toMatrix₂_mul
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.BilinForm LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix	—	LinearMap.toMatrix₂_mul_basis_toMatrix
toMatrix_symm 📖	mathematical	—	LinearEquiv.symm LinearMap.BilinForm Matrix CommSemiring.toSemiring LinearMap.addCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module RingHomInvPair.ids toMatrix Matrix.toBilin	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass
toMatrix_toBilin 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Matrix.toBilin	—	LinearEquiv.apply_symm_apply Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomInvPair.ids

LinearMap.BilinForm.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofSeparatingLeft 📖	mathematical	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule AddCommGroup.toAddCommMonoid RingHom.id	LinearMap.BilinForm.Nondegenerate	—	Module.Free.exists_basis Module.Finite.finite_basis IsDomain.toNontrivial Finite.of_fintype RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass LinearMap.BilinForm.nondegenerate_toMatrix_iff Matrix.nondegenerate_iff_det_ne_zero Matrix.separatingLeft_iff_det_ne_zero LinearMap.BilinForm.separatingLeft_toMatrix_iff
ofSeparatingRight 📖	mathematical	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule AddCommGroup.toAddCommMonoid RingHom.id	LinearMap.BilinForm.Nondegenerate	—	LinearMap.BilinForm.nondegenerate_flip_iff ofSeparatingLeft
toMatrix 📖	mathematical	LinearMap.BilinForm.Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Matrix.Nondegenerate Finite.of_fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix	—	Finite.of_fintype RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass LinearMap.BilinForm.nondegenerate_toMatrix_iff
toMatrix' 📖	mathematical	LinearMap.BilinForm.Nondegenerate CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module CommSemiring.toSemiring Semiring.toModule	Matrix.Nondegenerate Finite.of_fintype DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm NonAssocSemiring.toNonUnitalNonAssocSemiring Matrix LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix'	—	LinearMap.Nondegenerate.toMatrix₂'

LinearMap.BilinForm.SeparatingLeft

Theorems

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

LinearMap.BilinForm.SeparatingRight

Theorems

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

Matrix

Definitions

Name	Category	Theorems
toBilin 📖	CompOp	16 math math: LinearMap.BilinForm.toMatrix_toBilin, BilinForm.toMatrix_symm, separatingRight_toBilin_iff, toBilin_symm, toBilin_apply, BilinForm.toMatrix_toBilin, nondegenerate_toBilin'_iff_nondegenerate_toBilin, SeparatingLeft.toBilin, toBilin_basisFun, nondegenerate_toBilin_iff, Nondegenerate.toBilin, LinearMap.BilinForm.toMatrix_symm, toBilin_toMatrix, separatingLeft_toBilin_iff, SeparatingRight.toBilin, toBilin_comp
toBilin' 📖	CompOp	19 math math: SeparatingLeft.toBilin', LinearMap.BilinForm.toMatrix'_symm, nondegenerate_toBilin'_iff, toBilin'_symm, nondegenerate_toBilin'_iff_nondegenerate_toBilin, toBilin_basisFun, LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero, toBilin'_apply, toBilin'_comp, toBilin'_apply', separatingLeft_toBilin'_iff, toBilin'Aux_eq, separatingRight_toBilin'_iff, Nondegenerate.toBilin', LinearMap.BilinForm.toMatrix'_toBilin', SeparatingRight.toBilin', LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero', toBilin'_toMatrix', toBilin'_single
toBilin'Aux 📖	CompOp	4 math math: LinearMap.toBilin'Aux_toMatrixAux, toBilin'Aux_toMatrixAux, toBilin'Aux_single, toBilin'Aux_eq

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	—	isAdjointPair_equiv
nondegenerate_toBilin'_iff 📖	mathematical	—	LinearMap.BilinForm.Nondegenerate CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap.BilinForm addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin' Nondegenerate Finite.of_fintype	—	nondegenerate_toLinearMap₂'_iff
nondegenerate_toBilin'_iff_nondegenerate_toBilin 📖	mathematical	—	LinearMap.BilinForm.Nondegenerate Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap.BilinForm addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin' toBilin	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Finite.of_fintype LinearMap.BilinForm.nondegenerate_congr_iff
nondegenerate_toBilin_iff 📖	mathematical	—	LinearMap.BilinForm.Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap.BilinForm addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin Nondegenerate Finite.of_fintype	—	nondegenerate_toLinearMap₂_iff
separatingLeft_toBilin'_iff 📖	mathematical	—	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Pi.addCommMonoid Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap.BilinForm addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin' SeparatingLeft Finite.of_fintype	—	separatingLeft_toLinearMap₂'_iff
separatingLeft_toBilin_iff 📖	mathematical	—	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule AddCommGroup.toAddCommMonoid RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap.BilinForm addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin SeparatingLeft Finite.of_fintype	—	separatingLeft_toLinearMap₂_iff
separatingRight_toBilin'_iff 📖	mathematical	—	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Pi.addCommMonoid Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap.BilinForm addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin' SeparatingRight Finite.of_fintype	—	separatingRight_toLinearMap₂'_iff
separatingRight_toBilin_iff 📖	mathematical	—	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule AddCommGroup.toAddCommMonoid RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap.BilinForm addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin SeparatingRight Finite.of_fintype	—	separatingRight_toLinearMap₂_iff
toBilin'Aux_eq 📖	mathematical	—	toBilin'Aux DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin'	—	—
toBilin'Aux_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module toBilin'Aux Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toLinearMap₂'Aux_single
toBilin'_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.BilinForm LinearMap.addCommMonoid LinearMap.module LinearEquiv RingHomInvPair.ids Matrix addCommMonoid module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin' Finset.sum Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	RingHomInvPair.ids LinearMap.instSMulCommClass toLinearMap₂'_apply Finset.sum_congr mul_comm mul_left_comm
toBilin'_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.BilinForm LinearMap.addCommMonoid LinearMap.module LinearEquiv RingHomInvPair.ids Matrix addCommMonoid module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin' dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib mulVec	—	toLinearMap₂'_apply'
toBilin'_comp 📖	mathematical	—	LinearMap.BilinForm.comp Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap.BilinForm addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin' 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.BilinForm.toMatrix'_comp LinearMap.toMatrix'_toLin' LinearMap.BilinForm.toMatrix'_toBilin'
toBilin'_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearEquiv RingHomInvPair.ids Matrix addCommMonoid module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin' Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass toBilin'_apply Finset.sum_congr Pi.single_apply ite_mul one_mul MulZeroClass.zero_mul mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq'
toBilin'_symm 📖	mathematical	—	LinearEquiv.symm Matrix LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid LinearMap RingHom.id LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomInvPair.ids toBilin' LinearMap.BilinForm.toMatrix'	—	LinearEquiv.symm_symm Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomInvPair.ids
toBilin'_toMatrix' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin' LinearMap.BilinForm.toMatrix'	—	LinearEquiv.apply_symm_apply Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomInvPair.ids
toBilin_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearEquiv RingHomInvPair.ids Matrix addCommMonoid module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin Finset.sum Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr	—	smulCommClass_self RingHomInvPair.ids LinearMap.instSMulCommClass toLinearMap₂_apply Finset.sum_congr mul_comm mul_left_comm
toBilin_basisFun 📖	mathematical	—	toBilin Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule Pi.basisFun Finite.of_fintype toBilin'	—	LinearEquiv.ext Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomInvPair.ids Finite.of_fintype LinearMap.pi_ext' LinearMap.ext_ring RingHomCompTriple.ids toBilin_apply Finset.sum_congr Pi.basisFun_repr toBilin'_apply
toBilin_comp 📖	mathematical	—	LinearMap.BilinForm.comp DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap.BilinForm addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid toLin Finite.of_fintype instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib transpose	—	LinearMap.BilinForm.ext RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass smulCommClass_self Finite.of_fintype toBilin.eq_1 LinearMap.BilinForm.toMatrix.eq_1 LinearMap.toMatrix₂_symm toLinearMap₂_compl₁₂ toLinearMap₂_apply Finset.sum_congr
toBilin_symm 📖	mathematical	—	LinearEquiv.symm Matrix LinearMap.BilinForm CommSemiring.toSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap RingHom.id Semiring.toModule LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomInvPair.ids toBilin LinearMap.BilinForm.toMatrix	—	LinearEquiv.symm_symm Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomInvPair.ids
toBilin_toMatrix 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap.BilinForm addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toBilin LinearMap.BilinForm.toMatrix	—	LinearEquiv.apply_symm_apply Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomInvPair.ids

Matrix.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toBilin 📖	mathematical	Matrix.Nondegenerate Finite.of_fintype	LinearMap.BilinForm.Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap.BilinForm Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid LinearMap Semiring.toModule LinearMap.module Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toBilin	—	Finite.of_fintype toLinearMap₂
toBilin' 📖	mathematical	Matrix.Nondegenerate Finite.of_fintype	LinearMap.BilinForm.Nondegenerate CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap.BilinForm Matrix.addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toBilin'	—	Finite.of_fintype toLinearMap₂'

Matrix.SeparatingLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toBilin 📖	mathematical	Matrix.SeparatingLeft Finite.of_fintype	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule AddCommGroup.toAddCommMonoid RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap.BilinForm Matrix.addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toBilin	—	Finite.of_fintype toLinearMap₂
toBilin' 📖	mathematical	Matrix.SeparatingLeft Finite.of_fintype	LinearMap.SeparatingLeft CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Pi.addCommMonoid Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap.BilinForm Matrix.addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toBilin'	—	Finite.of_fintype toLinearMap₂'

Matrix.SeparatingRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toBilin 📖	mathematical	Matrix.SeparatingRight Finite.of_fintype	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule AddCommGroup.toAddCommMonoid RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap.BilinForm Matrix.addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toBilin	—	Finite.of_fintype toLinearMap₂
toBilin' 📖	mathematical	Matrix.SeparatingRight Finite.of_fintype	LinearMap.SeparatingRight CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Pi.addCommMonoid Pi.Function.module RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap.BilinForm Matrix.addCommMonoid LinearMap.addCommMonoid LinearMap LinearMap.module Matrix.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toBilin'	—	Finite.of_fintype toLinearMap₂'

(root)

Definitions

Name	Category	Theorems
selfAdjointMatricesSubmodule' 📖	CompOp	—
skewAdjointMatricesSubmodule' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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	—	—
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	—	—
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	—	—
toBilin'Aux_toMatrixAux 📖	mathematical	—	Matrix.toBilin'Aux DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.BilinForm Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid LinearMap.module Matrix.addCommMonoid Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module LinearMap.instFunLike LinearMap.BilinForm.toMatrixAux Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	LinearMap.toBilin'Aux_toMatrixAux

---

← Back to Index