FDeriv

Statistics

Metric	Count
Definitions	0
Theorems `fderiv_apply_scaleUnit`, `fderiv_dimension_const_direction`, `fderiv_isDimensionallyCorrect`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`fderiv_apply_scaleUnit` 📖	mathematical	`IsDimensionallyCorrect` `instUnitDependentTwoSided` `LinearUnitDependent.toUnitDependent` `instLinearUnitDependentOfHasDim`	`UnitDependent.scaleUnit` `Dimension` `Dimension.instCommGroup` `UnitChoices.dimScale` `dim`	—	`UnitChoices.dimScale_coe_mul_symm`
`fderiv_dimension_const_direction` 📖	mathematical	`IsDimensionallyCorrect` `instUnitDependentTwoSided` `LinearUnitDependent.toUnitDependent` `instLinearUnitDependentOfHasDim`	`instUnitDependentForall_1` `WithDim` `Dimension` `Dimension.instMul` `dim` `Dimension.instCommGroup` `MulUnitDependent.toUnitDependent` `CarriesDimension.toMulAction` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `instMulUnitDependent` `WithDim.val`	—	`fderiv_apply_scaleUnit`
`fderiv_isDimensionallyCorrect` 📖	mathematical	`IsDimensionallyCorrect` `instUnitDependentTwoSided` `LinearUnitDependent.toUnitDependent` `instLinearUnitDependentOfHasDim`	`ContinuousLinearUnitDependent.toLinearUnitDependent` `instContinuousLinearUnitDependentMap` `instContinuousLinearUnitDependentOfHasDimOfContinuousConstSMulReal`	—	`fderiv_apply_scaleUnit` `HasDim.scaleUnit_apply` `UnitChoices.dimScale_mul_symm`

---