Documentation Verification Report

Trace

📁 Source: Mathlib/Analysis/InnerProductSpace/Trace.lean

Statistics

Metric	Count
Definitions	0
Theorems `trace_rankOne`, `re_trace_eq_sum_eigenvalues`, `trace_eq_sum_eigenvalues`, `trace_eq_sum_inner`	4
Total	4

InnerProductSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trace_rankOne` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `toNormedSpace` `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` `ContinuousLinearMap.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.module` `CommRing.toCommMonoid` `Field.toCommRing` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `rankOne` `Inner.inner` `toInner`	—	`smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `RingHomCompTriple.ids` `IsBoundedSMul.continuousSMul` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `rankOne_def'` `ContinuousLinearMap.coe_comp` `LinearMap.trace_comp_comm'` `Module.Free.of_divisionRing` `Module.Free.self` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `ContinuousLinearMap.comp_toSpanSingleton` `LinearMap.trace_eq_sum_inner` `Finset.sum_congr` `Finset.univ_unique` `OrthonormalBasis.singleton_apply` `one_mul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one` `Finset.sum_const` `Finset.card_singleton` `one_smul`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trace_eq_sum_inner` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike` `trace` `Finset.sum` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Finset.univ` `Inner.inner` `InnerProductSpace.toInner` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `trace_eq_matrix_trace` `Fintype.sum_congr` `Matrix.diag_apply` `toMatrix_apply` `OrthonormalBasis.coe_toBasis` `fact_one_le_two_ennreal` `OrthonormalBasis.coe_toBasis_repr_apply` `OrthonormalBasis.repr_apply_apply`

LinearMap.IsSymmetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`re_trace_eq_sum_eigenvalues` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.IsSymmetric`	`DFunLike.coe` `AddMonoidHom` `Real` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `LinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Module.toDistribMulAction` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.trace` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `Fin.fintype` `eigenvalues`	—	`smulCommClass_self` `trace_eq_sum_eigenvalues` `RCLike.ofReal_re_ax`
`trace_eq_sum_eigenvalues` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.IsSymmetric`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `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` `RCLike.ofReal` `Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ` `Fin.fintype` `eigenvalues`	—	`smulCommClass_self` `LinearMap.trace_eq_sum_inner` `RCLike.ofReal_sum` `Fintype.sum_congr` `apply_eigenvectorBasis` `inner_smul_real_right` `inner_self_eq_norm_sq_to_K` `OrthonormalBasis.norm_eq_one` `RCLike.ofReal_alg` `one_smul` `one_pow`

---

← Back to Index