Documentation Verification Report

Defs

📁 Source: Mathlib/RingTheory/Trace/Defs.lean

Statistics

Metric	Count
Definitions `traceForm`	1
Theorems `traceForm_apply`, `traceForm_isSymm`, `traceForm_toMatrix`, `trace_algebraMap`, `trace_algebraMap_of_basis`, `trace_apply`, `trace_comp_trace`, `trace_comp_trace_of_basis`, `trace_eq_matrix_trace`, `trace_eq_zero_of_not_exists_basis`, `trace_prod`, `trace_prod_apply`, `trace_self`, `trace_self_apply`, `trace_trace`, `trace_trace_of_basis`	16
Total	17

Algebra

Definitions

Name	Category	Theorems
`traceForm` 📖	CompOp	18 math math: `integralClosure_le_span_dualBasis`, `traceForm_nondegenerate_tfae`, `traceMatrix_apply`, `traceForm_apply`, `Module.Basis.traceDual_def`, `traceForm_toMatrix`, `traceForm_dualSubmodule_adjoin`, `Submodule.restrictScalars_traceDual`, `FractionalIdeal.mem_dual`, `traceForm_isSymm`, `IsIntegralClosure.range_le_span_dualBasis`, `traceMatrix_of_basis`, `Submodule.mem_traceDual`, `traceForm_nondegenerate`, `Module.Basis.traceDual_repr_apply`, `traceForm_toMatrix_powerBasis`, `Submodule.mem_traceDual_iff_isIntegral`, `Module.Basis.traceDual_eq_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`traceForm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm` `trace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`traceForm_isSymm` 📖	mathematical	—	`LinearMap.BilinForm.IsSymm` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `CommSemiring.toSemiring` `traceForm`	—	`mul_comm`
`traceForm_toMatrix` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap.BilinForm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `Matrix` `LinearMap.addCommMonoid` `LinearMap` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Matrix.addCommMonoid` `to_smulCommClass` `id` `LinearMap.instSMulCommClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Matrix.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.BilinForm.toMatrix` `traceForm` `LinearMap.instFunLike` `trace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Module.Basis` `Module.Basis.instFunLike`	—	`RingHomInvPair.ids` `to_smulCommClass` `LinearMap.instSMulCommClass` `LinearMap.BilinForm.toMatrix_apply` `traceForm_apply`
`trace_algebraMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `Semiring.toModule` `LinearMap.instFunLike` `trace` `RingHom` `RingHom.instFunLike` `algebraMap` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Module.finrank`	—	`trace_algebraMap_of_basis` `Module.finrank_eq_card_basis` `trace_eq_zero_of_not_exists_basis` `finrank_eq_zero_of_not_exists_basis_finset` `zero_nsmul`
`trace_algebraMap_of_basis` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `Semiring.toModule` `LinearMap.instFunLike` `trace` `RingHom` `RingHom.instFunLike` `algebraMap` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Fintype.card`	—	`smulCommClass_self` `IsScalarTower.left` `trace_apply` `RingHomInvPair.ids` `Finite.of_fintype` `LinearMap.trace_eq_matrix_trace` `Matrix.trace.eq_1` `Finset.sum_congr` `AlgHom.commutes` `LinearMap.toMatrix_algebraMap` `Matrix.diagonal_apply_eq` `Finset.sum_const`
`trace_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `Semiring.toModule` `LinearMap.instFunLike` `trace` `LinearMap.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.trace` `AlgHom` `Module.End` `Module.End.instSemiring` `Module.End.instAlgebra` `toSMul` `id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `lmul`	—	—
`trace_comp_trace` 📖	mathematical	—	`LinearMap.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `trace` `LinearMap.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `toSMul` `IsScalarTower.right`	—	`LinearMap.ext` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `trace_trace`
`trace_comp_trace_of_basis` 📖	mathematical	—	`LinearMap.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `trace` `LinearMap.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `toSMul` `IsScalarTower.right`	—	`LinearMap.ext` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `LinearMap.comp_apply` `LinearMap.restrictScalars_apply` `trace_trace_of_basis`
`trace_eq_matrix_trace` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `Semiring.toModule` `LinearMap.instFunLike` `trace` `Matrix.trace` `AlgHom` `Matrix` `Matrix.semiring` `Matrix.instAlgebra` `id` `AlgHom.funLike` `leftMulMatrix`	—	`smulCommClass_self` `IsScalarTower.left` `trace_apply` `RingHomInvPair.ids` `Finite.of_fintype` `LinearMap.trace_eq_matrix_trace` `to_smulCommClass` `toMatrix_lmul_eq`
`trace_eq_zero_of_not_exists_basis` 📖	mathematical	`Module.Basis` `Finset` `SetLike.instMembership` `Finset.instSetLike` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule`	`trace` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Semiring.toModule` `LinearMap.instZero`	—	`LinearMap.ext` `smulCommClass_self` `to_smulCommClass` `IsScalarTower.right`
`trace_prod` 📖	mathematical	—	`trace` `Prod.instCommRing` `Prod.algebra` `CommRing.toCommSemiring` `Ring.toSemiring` `CommRing.toRing` `LinearMap.coprod` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `Semiring.toModule`	—	`LinearMap.ext` `LinearMap.coprod_apply` `trace_prod_apply`
`trace_prod_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Prod.instCommRing` `toModule` `Prod.algebra` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `LinearMap.instFunLike` `trace` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`smulCommClass_self` `IsScalarTower.left` `Prod.smulCommClass` `RingHomCompTriple.ids` `LinearMap.ext₂` `Prod.mul_def` `LinearMap.comp.congr_simp` `LinearMap.trace_prodMap'`
`trace_self` 📖	mathematical	—	`trace` `id` `CommRing.toCommSemiring` `LinearMap.id` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule`	—	`LinearMap.ext_ring` `Fintype.card_unique` `one_smul` `trace_algebraMap_of_basis`
`trace_self_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `id` `Semiring.toModule` `LinearMap.instFunLike` `trace`	—	`trace_self`
`trace_trace` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `Semiring.toModule` `LinearMap.instFunLike` `trace`	—	`trace_trace_of_basis` `Finite.of_fintype`
`trace_trace_of_basis` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `Semiring.toModule` `LinearMap.instFunLike` `trace`	—	`nonempty_fintype` `trace_eq_matrix_trace` `Matrix.trace.eq_1` `Finset.univ_product_univ` `Finset.sum_product` `Finset.sum_congr` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_apply` `smulTower_leftMulMatrix`

---

← Back to Index