Trace

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

Statistics

Metric	Count
Definitions `traceAddMonoidHom`, `traceLinearMap`	2
Theorems `map_trace`, `ext_iff_trace_mul_left`, `ext_iff_trace_mul_right`, `traceAddMonoidHom_apply`, `traceLinearMap_apply`, `trace_add`, `trace_blockDiagonal`, `trace_blockDiagonal'`, `trace_conjTranspose`, `trace_diagonal`, `trace_eq_zero_of_isEmpty`, `trace_fin_one`, `trace_fin_one_of`, `trace_fin_three`, `trace_fin_three_of`, `trace_fin_two`, `trace_fin_two_of`, `trace_fin_zero`, `trace_list_sum`, `trace_mul_comm`, `trace_mul_cycle`, `trace_mul_cycle'`, `trace_mul_single`, `trace_multiset_sum`, `trace_neg`, `trace_one`, `trace_replicateCol_mul_replicateRow`, `trace_single_eq_of_ne`, `trace_single_eq_same`, `trace_single_mul`, `trace_smul`, `trace_sub`, `trace_submatrix_succ`, `trace_sum`, `trace_surjective`, `trace_transpose`, `trace_transpose_mul`, `trace_units_conj`, `trace_units_conj'`, `trace_vecMulVec`, `trace_zero`	41
Total	43

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_trace` 📖	mathematical	—	`DFunLike.coe` `Matrix.trace` `Matrix.map`	—	`map_sum`

Matrix

Definitions

Name	Category	Theorems
`traceAddMonoidHom` 📖	CompOp	1 math math: `traceAddMonoidHom_apply`
`traceLinearMap` 📖	CompOp	1 math math: `traceLinearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_iff_trace_mul_left` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`ext` `trace_single_mul` `one_mul`
`ext_iff_trace_mul_right` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`ext` `trace_mul_single` `mul_one`
`traceAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Matrix` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `traceAddMonoidHom` `trace`	—	—
`traceLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `addCommMonoid` `module` `LinearMap.instFunLike` `traceLinearMap` `trace`	—	—
`trace_add` 📖	mathematical	—	`trace` `Matrix` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Finset.sum_add_distrib`
`trace_blockDiagonal` 📖	mathematical	—	`trace` `instFintypeProd` `blockDiagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum` `Finset.univ`	—	`Finset.sum_congr` `Fintype.sum_prod_type` `Finset.sum_comm`
`trace_blockDiagonal'` 📖	mathematical	—	`trace` `Sigma.instFintype` `blockDiagonal'` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum` `Finset.univ`	—	`Finset.sum_congr` `Finset.sum_sigma'`
`trace_conjTranspose` 📖	mathematical	—	`trace` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Star.star`	—	`star_sum`
`trace_diagonal` 📖	mathematical	—	`trace` `diagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum` `Finset.univ`	—	`Finset.sum_congr` `diagonal_apply_eq`
`trace_eq_zero_of_isEmpty` 📖	mathematical	—	`trace` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_congr` `Finset.univ_eq_empty`
`trace_fin_one` 📖	mathematical	—	`trace` `Fin.fintype`	—	`add_zero`
`trace_fin_one_of` 📖	mathematical	—	`trace` `Fin.fintype` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty`	—	`trace_fin_one`
`trace_fin_three` 📖	mathematical	—	`trace` `Fin.fintype` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`add_zero` `add_assoc`
`trace_fin_three_of` 📖	mathematical	—	`trace` `Fin.fintype` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`trace_fin_three`
`trace_fin_two` 📖	mathematical	—	`trace` `Fin.fintype` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`add_zero`
`trace_fin_two_of` 📖	mathematical	—	`trace` `Fin.fintype` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`trace_fin_two`
`trace_fin_zero` 📖	mathematical	—	`trace` `Fin.fintype` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`trace_list_sum` 📖	mathematical	—	`trace` `Matrix` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`map_list_sum` `AddMonoidHom.instAddMonoidHomClass`
`trace_mul_comm` 📖	mathematical	—	`trace` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `CommMagma.toMul`	—	`trace_transpose` `trace_transpose_mul` `transpose_mul`
`trace_mul_cycle` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`trace_mul_comm` `mul_assoc`
`trace_mul_cycle'` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_assoc` `trace_mul_comm`
`trace_mul_single` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `MulOpposite` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulOpposite.instZero` `MulZeroClass.toOppositeSMulWithZero` `MulOpposite.op`	—	`Finset.sum_congr` `ite_and` `mul_ite` `MulZeroClass.mul_zero` `Finset.sum_ite_eq`
`trace_multiset_sum` 📖	mathematical	—	`trace` `Multiset.sum` `Matrix` `addCommMonoid` `Multiset.map`	—	`map_multiset_sum` `AddMonoidHom.instAddMonoidHomClass`
`trace_neg` 📖	mathematical	—	`trace` `AddCommGroup.toAddCommMonoid` `Matrix` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Finset.sum_neg_distrib`
`trace_one` 📖	mathematical	—	`trace` `AddCommMonoidWithOne.toAddCommMonoid` `Matrix` `one` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toOne` `AddMonoidWithOne.toNatCast` `Fintype.card`	—	`Finset.sum_congr` `diag_one` `Finset.sum_const` `nsmul_one`
`trace_replicateCol_mul_replicateRow` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Unique.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `replicateCol` `replicateRow` `dotProduct`	—	`Finset.sum_congr` `Finset.univ_unique` `Finset.sum_const` `Finset.card_singleton` `one_smul`
`trace_single_eq_of_ne` 📖	mathematical	—	`trace` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_congr` `diag_single_of_ne` `Finset.sum_const_zero`
`trace_single_eq_same` 📖	mathematical	—	`trace` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_congr` `diag_single_same` `Finset.sum_pi_single'`
`trace_single_mul` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul`	—	`Finset.sum_congr` `ite_and` `ite_mul` `MulZeroClass.zero_mul` `Finset.sum_ite_irrel` `Finset.sum_ite_eq` `Finset.sum_const_zero`
`trace_smul` 📖	mathematical	—	`trace` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass`	—	`Finset.smul_sum`
`trace_sub` 📖	mathematical	—	`trace` `AddCommGroup.toAddCommMonoid` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Finset.sum_sub_distrib`
`trace_submatrix_succ` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `trace` `Fin.fintype` `submatrix`	—	`Equiv.sum_comp` `Finset.sum_congr` `Fintype.sum_option` `finSuccEquiv_symm_none` `finSuccEquiv_symm_some`
`trace_sum` 📖	mathematical	—	`trace` `Finset.sum` `Matrix` `addCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`trace_surjective` 📖	mathematical	—	`Matrix` `trace`	—	`trace_single_eq_same`
`trace_transpose` 📖	mathematical	—	`trace` `transpose`	—	—
`trace_transpose_mul` 📖	mathematical	—	`trace` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `transpose`	—	`Finset.sum_comm`
`trace_units_conj` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Units` `Units.instInv`	—	`trace_mul_cycle` `Units.inv_mul` `one_mul`
`trace_units_conj'` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Units` `Units.instInv`	—	`trace_units_conj`
`trace_vecMulVec` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `dotProduct`	—	`vecMulVec_eq` `trace_replicateCol_mul_replicateRow`
`trace_zero` 📖	mathematical	—	`trace` `Matrix` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_const` `smul_zero`

---

← Back to Index