Integral

📁 Source: PhysLean/Units/Integral.lean

Statistics

Metric	Count
Definitions instMulUnitDependentMeasureOfHasDimOfMeasurableConstSMulReal	1
Theorems integral_isDimensionallyCorrect, scaleUnit_measure	2
Total	3

(root)

Definitions

Name	Category	Theorems
instMulUnitDependentMeasureOfHasDimOfMeasurableConstSMulReal 📖	CompOp	2 math math: integral_isDimensionallyCorrect, scaleUnit_measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_isDimensionallyCorrect 📖	mathematical	—	IsDimensionallyCorrect instUnitDependentTwoSided DimSet instMulUnitDependentMeasureOfHasDimOfMeasurableConstSMulReal MulUnitDependent.toUnitDependent CarriesDimension.toMulAction instCarriesDimensionElemDimSet instMulUnitDependent instUnitDependentTwoSidedMul LinearUnitDependent.toUnitDependent instLinearUnitDependentOfHasDim Dimension Dimension.instMul dim Dimension.instCommGroup	—	scaleUnit_dimSet_val HasDim.scaleUnit_apply UnitChoices.dimScale_of_inv_eq_swap UnitChoices.dimScale_mul_symm
scaleUnit_measure 📖	mathematical	—	UnitDependent.scaleUnit MulUnitDependent.toUnitDependent instMulUnitDependentMeasureOfHasDimOfMeasurableConstSMulReal LinearUnitDependent.toUnitDependent instLinearUnitDependentOfHasDim	—	—

---

← Back to Index