Module

Statistics

Metric	Count
Definitions	0
Theorems `instContinuousConstSMulSubtypeLeOfNat`, `instContinuousSMulSubtypeLeOfNat`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousConstSMulSubtypeLeOfNat` 📖	mathematical	—	`ContinuousConstSMul` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nonneg.instSMul`	—	`ContinuousConstSMul.continuous_const_smul`
`instContinuousSMulSubtypeLeOfNat` 📖	mathematical	—	`ContinuousSMul` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nonneg.instSMul` `instTopologicalSpaceSubtype`	—	`Continuous.comp` `ContinuousSMul.continuous_smul` `Continuous.prodMap` `continuous_subtype_val` `continuous_id`

---