PEquiv

📁 Source: Mathlib/Data/Matrix/PEquiv.lean

Statistics

Metric	Count
Definitions toMatrix	1
Theorems map_toMatrix, mul_toMatrix_apply, mul_toMatrix_toPEquiv, single_mul_single, single_mul_single_of_ne, single_mul_single_right, toMatrix_apply, toMatrix_bot, toMatrix_injective, toMatrix_mul_apply, toMatrix_refl, toMatrix_swap, toMatrix_symm, toMatrix_toPEquiv_apply, toMatrix_toPEquiv_eq, toMatrix_toPEquiv_mul, toMatrix_toPEquiv_mulVec, toMatrix_trans, transpose_toMatrix_toPEquiv_apply, vecMul_toMatrix_toPEquiv	20
Total	21

PEquiv

Definitions

Name	Category	Theorems
toMatrix 📖	CompOp	20 math math: vecMul_toMatrix_toPEquiv, toMatrix_symm, single_mul_single_of_ne, toMatrix_toPEquiv_mulVec, map_toMatrix, toMatrix_toPEquiv_eq, toMatrix_bot, mul_toMatrix_apply, toMatrix_toPEquiv_mul, single_mul_single_right, toMatrix_injective, toMatrix_refl, toMatrix_apply, toMatrix_mul_apply, transpose_toMatrix_toPEquiv_apply, mul_toMatrix_toPEquiv, toMatrix_toPEquiv_apply, toMatrix_trans, toMatrix_swap, single_mul_single

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_toMatrix 📖	mathematical	—	Matrix.map toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe RingHom RingHom.instFunLike	—	Matrix.ext MonoidWithZeroHom.map_ite_one_zero RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
mul_toMatrix_apply 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe PEquiv instFunLikeOption symm	—	Finset.sum_congr eq_some_iff MulZeroClass.mul_zero Finset.sum_const_zero Finset.sum_eq_single mul_ite mul_one instIsEmptyFalse
mul_toMatrix_toPEquiv 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Equiv.toPEquiv Matrix.submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	Matrix.ext mul_toMatrix_apply Equiv.toPEquiv_symm Equiv.toPEquiv_apply Matrix.submatrix_apply
single_mul_single 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne single	—	toMatrix_trans single_trans_single
single_mul_single_of_ne 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne single Matrix.zero	—	toMatrix_trans single_trans_single_of_ne toMatrix_bot
single_mul_single_right 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne single	—	Matrix.mul_assoc single_mul_single
toMatrix_apply 📖	mathematical	—	toMatrix DFunLike.coe PEquiv instFunLikeOption	—	—
toMatrix_bot 📖	mathematical	—	toMatrix Bot.bot PEquiv instBotPEquiv Matrix Matrix.zero	—	—
toMatrix_injective 📖	mathematical	—	PEquiv Matrix toMatrix MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	not_imp_not Matrix.ext_iff NeZero.one
toMatrix_mul_apply 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe PEquiv instFunLikeOption	—	Finset.sum_congr MulZeroClass.zero_mul Finset.sum_const_zero Finset.sum_eq_single one_mul instIsEmptyFalse
toMatrix_refl 📖	mathematical	—	toMatrix refl Matrix Matrix.one	—	Matrix.ext
toMatrix_swap 📖	mathematical	—	toMatrix NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Equiv.toPEquiv Equiv.swap Matrix Matrix.add AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid Matrix.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid Matrix.one single	—	Matrix.ext sub_self zero_sub neg_add_cancel zero_add add_zero sub_zero
toMatrix_symm 📖	mathematical	—	toMatrix symm Matrix.transpose	—	Matrix.ext mem_iff_mem
toMatrix_toPEquiv_apply 📖	mathematical	—	toMatrix Equiv.toPEquiv Pi.single DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	Pi.single_apply
toMatrix_toPEquiv_eq 📖	mathematical	—	toMatrix Equiv.toPEquiv Matrix.submatrix Matrix Matrix.one DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	Matrix.ext if_congr
toMatrix_toPEquiv_mul 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Equiv.toPEquiv Matrix.submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	Matrix.ext toMatrix_mul_apply Equiv.toPEquiv_apply Matrix.submatrix_apply
toMatrix_toPEquiv_mulVec 📖	mathematical	—	Matrix.mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Equiv.toPEquiv DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	Finset.sum_congr ite_mul one_mul MulZeroClass.zero_mul Finset.sum_ite_eq
toMatrix_trans 📖	mathematical	—	toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne trans Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid	—	Matrix.ext toMatrix_mul_apply
transpose_toMatrix_toPEquiv_apply 📖	mathematical	—	Matrix.transpose toMatrix Equiv.toPEquiv Pi.single DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	Pi.single_apply
vecMul_toMatrix_toPEquiv 📖	mathematical	—	Matrix.vecMul NonAssocSemiring.toNonUnitalNonAssocSemiring toMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Equiv.toPEquiv DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	Finset.sum_congr Equiv.apply_eq_iff_eq_symm_apply mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq'

---

← Back to Index