Reindex

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

Statistics

Metric	Count
Definitions reindexAlgEquiv, reindexLinearEquiv	2
Theorems det_reindexAlgEquiv, det_reindexLinearEquiv_self, mul_reindexLinearEquiv_one, reindexAlgEquiv_apply, reindexAlgEquiv_mul, reindexAlgEquiv_refl, reindexAlgEquiv_symm, reindexLinearEquiv_apply, reindexLinearEquiv_comp, reindexLinearEquiv_comp_apply, reindexLinearEquiv_mul, reindexLinearEquiv_one, reindexLinearEquiv_refl_refl, reindexLinearEquiv_symm, reindexLinearEquiv_trans	15
Total	17

Matrix

Definitions

Name	Category	Theorems
reindexAlgEquiv 📖	CompOp	8 math math: det_reindexAlgEquiv, TransvectionStruct.toMatrix_reindexEquiv_prod, TransvectionStruct.toMatrix_reindexEquiv, reindexAlgEquiv_mul, reindexAlgEquiv_symm, reindexAlgEquiv_refl, reindexAlgEquiv_apply, Module.Basis.toMatrix_reindex'
reindexLinearEquiv 📖	CompOp	10 math math: reindexLinearEquiv_trans, mul_reindexLinearEquiv_one, reindexLinearEquiv_one, reindexLinearEquiv_comp, reindexLinearEquiv_mul, reindexLinearEquiv_apply, reindexLinearEquiv_symm, det_reindexLinearEquiv_self, reindexLinearEquiv_refl_refl, reindexLinearEquiv_comp_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_reindexAlgEquiv 📖	mathematical	—	det DFunLike.coe AlgEquiv Matrix semiring CommSemiring.toSemiring CommRing.toCommSemiring instAlgebra AlgEquiv.instFunLike reindexAlgEquiv	—	det_reindex_self
det_reindexLinearEquiv_self 📖	mathematical	—	det DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reindexLinearEquiv	—	det_reindex_self
mul_reindexLinearEquiv_one 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids addCommMonoid module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reindexLinearEquiv one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Equiv.refl Equiv.trans Equiv.symm	—	mul_submatrix_one Finite.of_fintype
reindexAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix semiring instAlgebra AlgEquiv.instFunLike reindexAlgEquiv Equiv EquivLike.toFunLike Equiv.instEquivLike reindex	—	—
reindexAlgEquiv_mul 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix semiring instAlgebra AlgEquiv.instFunLike reindexAlgEquiv instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid	—	map_mul NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass
reindexAlgEquiv_refl 📖	mathematical	—	reindexAlgEquiv Equiv.refl AlgEquiv.refl Matrix semiring instAlgebra	—	AlgEquiv.ext
reindexAlgEquiv_symm 📖	mathematical	—	AlgEquiv.symm Matrix semiring instAlgebra reindexAlgEquiv Equiv.symm	—	—
reindexLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix addCommMonoid module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reindexLinearEquiv Equiv Equiv.instEquivLike reindex	—	RingHomInvPair.ids
reindexLinearEquiv_comp 📖	mathematical	—	Matrix DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids addCommMonoid module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reindexLinearEquiv Equiv.trans	—	RingHomInvPair.ids RingHomCompTriple.ids reindexLinearEquiv_trans
reindexLinearEquiv_comp_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix addCommMonoid module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reindexLinearEquiv Equiv.trans	—	submatrix_submatrix
reindexLinearEquiv_mul 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids addCommMonoid module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reindexLinearEquiv	—	submatrix_mul_equiv
reindexLinearEquiv_one 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix addCommMonoid module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reindexLinearEquiv one AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	submatrix_one_equiv
reindexLinearEquiv_refl_refl 📖	mathematical	—	reindexLinearEquiv Equiv.refl LinearEquiv.refl Matrix addCommMonoid module	—	LinearEquiv.ext RingHomInvPair.ids
reindexLinearEquiv_symm 📖	mathematical	—	LinearEquiv.symm Matrix addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids reindexLinearEquiv Equiv.symm	—	RingHomInvPair.ids
reindexLinearEquiv_trans 📖	mathematical	—	LinearEquiv.trans Matrix addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids reindexLinearEquiv Equiv.trans	—	LinearEquiv.ext RingHomInvPair.ids RingHomCompTriple.ids ext

---

← Back to Index