Documentation Verification Report

FiniteDimensionBilinear

📁 Source: Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean

Statistics

Metric	Count
Definitions `evalL`, `toContinuousBilinearMap`, `toContinuousBilinearMap`	3
Theorems `evalL_apply`, `toContinuousBilinearMap_apply`, `toContinuousBilinearMap_apply`	3
Total	6

ContinuousLinearMap

Definitions

Name	Category	Theorems
`evalL` 📖	CompOp	1 math math: `evalL_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evalL_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `topologicalSpace` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `funLike` `addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `evalL`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`

IsBilinearMap

Definitions

Name	Category	Theorems
`toContinuousBilinearMap` 📖	CompOp	1 math math: `toContinuousBilinearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContinuousBilinearMap_apply` 📖	mathematical	`IsBilinearMap` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toContinuousBilinearMap`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`

LinearMap

Definitions

Name	Category	Theorems
`toContinuousBilinearMap` 📖	CompOp	1 math math: `toContinuousBilinearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContinuousBilinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toContinuousBilinearMap` `LinearMap` `instFunLike` `addCommMonoid` `module`	—	`smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousSMul.continuousConstSMul`

---

← Back to Index