Trace

📁 Source: Mathlib/LinearAlgebra/Trace.lean

Statistics

Metric	Count
Definitions `traceAux`	1
Theorems `isNilpotent_trace_of_isNilpotent`, `traceAux_def`, `traceAux_eq`, `trace_baseChange`, `trace_comp_comm`, `trace_comp_comm'`, `trace_comp_cycle`, `trace_comp_cycle'`, `trace_comp_eq_mul_of_commute_of_isNilpotent`, `trace_conj`, `trace_conj'`, `trace_eq_contract`, `trace_eq_contract'`, `trace_eq_contract_apply`, `trace_eq_contract_of_basis`, `trace_eq_contract_of_basis'`, `trace_eq_matrix_trace`, `trace_eq_matrix_trace_of_finset`, `trace_id`, `trace_lie`, `trace_map`, `trace_mul_comm`, `trace_mul_cycle`, `trace_mul_cycle'`, `trace_one`, `trace_prodMap`, `trace_prodMap'`, `trace_smulRight`, `trace_tensorProduct`, `trace_tensorProduct'`, `trace_transpose`, `trace_transpose'`, `trace_map`, `trace_toLin'_eq`, `trace_toLin_eq`	35
Total	36

LinearMap

Definitions

Name	Category	Theorems
`traceAux` 📖	CompOp	2 math math: `traceAux_def`, `traceAux_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNilpotent_trace_of_isNilpotent` 📖	mathematical	`IsNilpotent` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instZero` `Monoid.toNatPow` `Module.End.instMonoid`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DFunLike.coe` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace`	—	`smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `trace_eq_matrix_trace` `Matrix.isNilpotent_trace_of_isNilpotent` `trace.eq_1` `IsNilpotent.zero`
`traceAux_def` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `traceAux` `Matrix.trace` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `Matrix.addCommMonoid` `Matrix.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toMatrix` `Finite.of_fintype`	—	`smulCommClass_self`
`traceAux_eq` 📖	mathematical	—	`traceAux`	—	`ext` `smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `RingHomCompTriple.ids` `RingHomCompTriple.right_ids` `id_comp` `comp_id` `toMatrix_comp` `Matrix.mul_assoc` `Matrix.trace_mul_comm`
`trace_baseChange` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `addCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instFunLike` `trace` `baseChange` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `RingHomInvPair.ids` `Finite.of_fintype` `trace_eq_matrix_trace` `toMatrix_baseChange` `AddMonoidHom.map_trace` `AddMonoidHom.instAddMonoidHomClass`
`trace_comp_comm` 📖	mathematical	—	`compr₂` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instSMulCommClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.to_smulCommClass` `Algebra.id` `IsScalarTower.right` `instIsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `IsScalarTower.left` `llcomp` `RingHomCompTriple.ids` `trace` `SMulCommClass.symm` `flip`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `instSMulCommClass` `IsScalarTower.right` `instIsScalarTower` `IsScalarTower.left` `RingHomCompTriple.ids` `SMulCommClass.symm` `LinearEquiv.surjective` `RingHomInvPair.ids` `TensorProduct.AlgebraTensorModule.curry_injective` `ext` `IsScalarTower.to_smulCommClass` `comp_dualTensorHom` `LinearMapClass.map_smul` `semilinearMapClass` `trace_eq_contract_apply` `mul_comm`
`trace_comp_comm'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `comp` `RingHomCompTriple.ids`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `instSMulCommClass` `IsScalarTower.right` `instIsScalarTower` `IsScalarTower.left` `RingHomCompTriple.ids` `SMulCommClass.symm` `ext_iff` `trace_comp_comm`
`trace_comp_cycle` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `comp` `RingHomCompTriple.ids`	—	`smulCommClass_self` `RingHomCompTriple.ids` `trace_comp_comm'` `comp_assoc`
`trace_comp_cycle'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `comp` `RingHomCompTriple.ids`	—	`smulCommClass_self` `RingHomCompTriple.ids` `trace_comp_comm'` `comp_assoc`
`trace_comp_eq_mul_of_commute_of_isNilpotent` 📖	mathematical	`Commute` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `IsNilpotent` `instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `instSub` `DFunLike.coe` `RingHom` `Module.End.instSemiring` `RingHom.instFunLike` `algebraMap` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`LinearMap` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `CommSemiring.toCommMonoid` `Semiring.toModule` `instFunLike` `trace` `comp` `RingHomCompTriple.ids` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`smulCommClass_self` `IsScalarTower.left` `RingHomCompTriple.ids` `isNilpotent_iff_eq_zero` `Module.End.mul_eq_comp` `isNilpotent_trace_of_isNilpotent` `Commute.isNilpotent_mul_left` `Commute.sub_right` `Algebra.commute_algebraMap_right` `eq_add_of_sub_eq'` `ext` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `semilinearMapClass` `comp_add` `map_add` `SemilinearMapClass.toAddHomClass` `add_zero` `smul_eq_mul`
`trace_conj` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `Module.End.instMul` `Units.val` `Module.End.instMonoid` `Units` `Units.instInv`	—	`smulCommClass_self` `trace_mul_comm` `Units.inv_mul_cancel_left`
`trace_conj'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `LinearEquiv` `RingHomInvPair.ids` `Module.End` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.conj`	—	`RingHomInvPair.ids` `smulCommClass_self` `RingHomInvPair.triples₂` `RingHomCompTriple.ids` `LinearEquiv.conj_apply` `trace_comp_comm'` `Module.free_def` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Module.Finite.of_basis` `Finite.of_fintype` `comp_assoc` `LinearEquiv.comp_coe` `LinearEquiv.self_trans_symm` `LinearEquiv.refl_toLinearMap` `RingHomCompTriple.right_ids` `id_comp` `trace.eq_1` `Finset.coe_image` `zero_apply`
`trace_eq_contract` 📖	mathematical	—	`comp` `TensorProduct` `CommRing.toCommSemiring` `Module.Dual` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHomCompTriple.ids` `trace` `dualTensorHom` `contractLeft`	—	`trace_eq_contract_of_basis` `Finite.of_fintype`
`trace_eq_contract'` 📖	mathematical	—	`trace` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `comp` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `Module.Dual` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `Algebra.to_smulCommClass` `Algebra.id` `TensorProduct.addCommMonoid` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.instModule` `RingHomCompTriple.ids` `contractLeft` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `dualTensorHomEquiv`	—	`trace_eq_contract_of_basis'`
`trace_eq_contract_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `TensorProduct` `Module.Dual` `Algebra.to_smulCommClass` `Algebra.id` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `dualTensorHom` `contractLeft`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `RingHomCompTriple.ids` `comp_apply` `trace_eq_contract`
`trace_eq_contract_of_basis` 📖	mathematical	—	`comp` `TensorProduct` `CommRing.toCommSemiring` `Module.Dual` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHomCompTriple.ids` `trace` `dualTensorHom` `contractLeft`	—	`nonempty_fintype` `Algebra.to_smulCommClass` `smulCommClass_self` `RingHomCompTriple.ids` `Module.Basis.ext` `IsScalarTower.to_smulCommClass` `instIsScalarTower` `IsScalarTower.right` `Module.Basis.tensorProduct_apply` `Module.Basis.coe_dualBasis` `RingHomInvPair.ids` `Finite.of_fintype` `trace_eq_matrix_trace` `toMatrix_dualTensorHom` `eq_or_ne` `Matrix.trace_single_eq_same` `Module.Basis.repr_self` `Finsupp.single_eq_same` `Matrix.trace_single_eq_of_ne` `Finsupp.single_eq_of_ne`
`trace_eq_contract_of_basis'` 📖	mathematical	—	`trace` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `comp` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `Module.Dual` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `Algebra.to_smulCommClass` `Algebra.id` `TensorProduct.addCommMonoid` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.instModule` `RingHomCompTriple.ids` `contractLeft` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `dualTensorHomEquivOfBasis`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `trace_eq_contract_of_basis` `Finite.of_fintype`
`trace_eq_matrix_trace` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `Matrix.trace` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `Matrix.addCommMonoid` `Matrix.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toMatrix` `Finite.of_fintype`	—	`smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `trace_eq_matrix_trace_of_finset` `traceAux_def` `traceAux_eq`
`trace_eq_matrix_trace_of_finset` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `Matrix.trace` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Subtype.fintype` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `Matrix.addCommMonoid` `Matrix.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toMatrix` `Finite.of_fintype`	—	`smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `trace.eq_1` `traceAux_def` `traceAux_eq`
`trace_id` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `id` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Module.finrank`	—	`smulCommClass_self` `Module.End.one_eq_id` `trace_one`
`trace_lie` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `Bracket.bracket` `Module.End` `Ring.instBracket` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.End.instRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`smulCommClass_self` `Ring.lie_def` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `trace_mul_comm` `sub_self`
`trace_map` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `EquivLike.toFunLike`	—	`smulCommClass_self` `IsScalarTower.left` `RingHomInvPair.ids` `AlgEquiv.eq_linearEquivConjAlgEquiv` `Module.Projective.of_free` `Module.Free.of_divisionRing` `trace_conj'`
`trace_mul_comm` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `Module.End.instMul`	—	`smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `trace_eq_matrix_trace` `toMatrix_mul` `Matrix.trace_mul_comm` `trace.eq_1` `zero_apply`
`trace_mul_cycle` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `Module.End.instMul`	—	`smulCommClass_self` `trace_mul_comm` `mul_assoc`
`trace_mul_cycle'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `Module.End.instMul`	—	`smulCommClass_self` `mul_assoc` `trace_mul_comm`
`trace_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `Module.End.instOne` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Module.finrank`	—	`subsingleton_or_nontrivial` `smulCommClass_self` `Module.finrank_subsingleton` `Nat.cast_one` `RingHomInvPair.ids` `Finite.of_fintype` `trace_eq_matrix_trace` `toMatrix_one` `Module.finrank_eq_card_chooseBasisIndex` `commRing_strongRankCondition` `Matrix.trace_one`
`trace_prodMap` 📖	mathematical	—	`comp` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddCommMonoid` `Prod.instModule` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `CommSemiring.toCommMonoid` `Semiring.toModule` `RingHomCompTriple.ids` `trace` `prodMapLinear` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `coprod` `id` `prodMap`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `smulCommClass_self` `LinearEquiv.surjective` `RingHomCompTriple.ids` `cancel_right` `prod_ext` `TensorProduct.AlgebraTensorModule.curry_injective` `instIsScalarTower` `IsScalarTower.right` `ext` `IsScalarTower.to_smulCommClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `dualTensorHom_prodMap_zero` `trace_eq_contract_apply` `Module.Free.prod` `Module.Finite.prod` `add_zero` `zero_prodMap_dualTensorHom` `zero_add`
`trace_prodMap'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `prodMap` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`smulCommClass_self` `RingHomCompTriple.ids` `ext_iff` `trace_prodMap`
`trace_smulRight` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `smulRight` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`smulCommClass_self` `IsScalarTower.left` `RingHomInvPair.ids` `Finite.of_fintype` `trace_eq_matrix_trace` `Module.Basis.sum_repr` `toMatrix_smulRight` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Module.Basis.repr_self` `Finsupp.smul_single` `mul_one` `Finsupp.univ_sum_single` `Matrix.trace_vecMulVec` `semilinearMapClass`
`trace_tensorProduct` 📖	mathematical	—	`compr₂` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Semiring.toModule` `instSMulCommClass` `DistribMulAction.toDistribSMul` `Algebra.to_smulCommClass` `Algebra.id` `IsScalarTower.right` `instIsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `TensorProduct.isScalarTower` `IsScalarTower.left` `TensorProduct.mapBilinear` `trace` `compl₁₂` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `lsmul`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `TensorProduct.smulCommClass_left` `instSMulCommClass` `IsScalarTower.right` `instIsScalarTower` `TensorProduct.isScalarTower` `IsScalarTower.left` `LinearEquiv.surjective` `RingHomInvPair.ids` `TensorProduct.AlgebraTensorModule.curry_injective` `ext` `IsScalarTower.to_smulCommClass` `map_dualTensorHom` `trace_eq_contract_apply` `Module.Free.tensor` `Module.Finite.tensorProduct`
`trace_tensorProduct'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `TensorProduct.map` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `TensorProduct.smulCommClass_left` `instSMulCommClass` `IsScalarTower.right` `instIsScalarTower` `TensorProduct.isScalarTower` `IsScalarTower.left` `ext_iff` `trace_tensorProduct`
`trace_transpose` 📖	mathematical	—	`comp` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.Dual` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `Algebra.to_smulCommClass` `Algebra.id` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHomCompTriple.ids` `trace` `Module.Dual.transpose`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `smulCommClass_self` `LinearEquiv.surjective` `RingHomCompTriple.ids` `cancel_right` `TensorProduct.AlgebraTensorModule.curry_injective` `instIsScalarTower` `IsScalarTower.right` `ext` `IsScalarTower.to_smulCommClass` `transpose_dualTensorHom` `trace_eq_contract_apply` `Module.dual_free` `Module.dual_finite` `Module.Projective.of_free` `trace_eq_contract`
`trace_transpose'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.Dual` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instFunLike` `trace` `instSMulCommClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.Dual.transpose`	—	`smulCommClass_self` `instSMulCommClass` `RingHomCompTriple.ids` `comp_apply` `Algebra.to_smulCommClass` `trace_transpose`

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trace_map` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `Matrix` `EquivLike.toFunLike`	—	`smulCommClass_self` `Function.smulCommClass` `Algebra.to_smulCommClass` `Pi.isScalarTower` `IsScalarTower.right` `RingHomInvPair.ids` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `LinearMap.toMatrix'_one` `LinearMap.toMatrix'_mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `AlgEquivClass.toRingEquivClass` `LinearMap.toMatrix'_toLin'` `trace_toLin'_eq` `LinearMap.trace_map`
`trace_toLin'_eq` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `LinearMap.trace` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin'` `trace`	—	`trace_toLin_eq` `Finite.of_fintype`
`trace_toLin_eq` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.trace` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin` `Finite.of_fintype` `trace`	—	`smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `LinearMap.trace_eq_matrix_trace` `LinearMap.toMatrix_toLin`

---

← Back to Index