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.toPow Module.End.instMonoid	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe 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 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.toPow 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	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 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