Documentation Verification Report

Area

📁 Source: PhysLean/Units/WithDim/Area.lean

Statistics

Metric	Count
Definitions `DimArea`, `acre`, `are`, `hectare`, `squareFoot`, `squareMeter`, `squareMile`	7
Theorems `acre_eq_mul_squareFeet`, `acre_in_SI`, `are_in_SI`, `hectare_in_SI`, `squareFoot_in_SI`, `squareMeter_in_SI`, `squareMile_in_SI`	7
Total	14

DimArea

Definitions

Name	Category	Theorems
`acre` 📖	CompOp	2 math math: `acre_eq_mul_squareFeet`, `acre_in_SI`
`are` 📖	CompOp	1 math math: `are_in_SI`
`hectare` 📖	CompOp	1 math math: `hectare_in_SI`
`squareFoot` 📖	CompOp	2 math math: `squareFoot_in_SI`, `acre_eq_mul_squareFeet`
`squareMeter` 📖	CompOp	1 math math: `squareMeter_in_SI`
`squareMile` 📖	CompOp	1 math math: `squareMile_in_SI`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acre_eq_mul_squareFeet` 📖	mathematical	—	`acre` `DimArea` `instMulActionNNRealDimensionful` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `squareFoot`	—	`acre_in_SI` `squareFoot_in_SI` `WithDim.ext`
`acre_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `acre` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `LengthUnit.scale_div_self` `TimeUnit.div_self` `MassUnit.div_self` `ChargeUnit.div_self` `TemperatureUnit.div_self` `Dimension.L𝓭_length` `WithDim.ext`
`are_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `are` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `UnitChoices.dimScale_self`
`hectare_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `hectare` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `UnitChoices.dimScale_self`
`squareFoot_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `squareFoot` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `LengthUnit.scale_div_self` `TimeUnit.div_self` `MassUnit.div_self` `ChargeUnit.div_self` `TemperatureUnit.div_self` `Dimension.L𝓭_length` `WithDim.ext`
`squareMeter_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `squareMeter` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `UnitChoices.dimScale_self`
`squareMile_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `squareMile` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `LengthUnit.scale_div_self` `TimeUnit.div_self` `MassUnit.div_self` `ChargeUnit.div_self` `TemperatureUnit.div_self` `Dimension.L𝓭_length` `WithDim.ext`

(root)

Definitions

Name	Category	Theorems
`DimArea` 📖	CompOp	1 math math: `DimArea.acre_eq_mul_squareFeet`

---

← Back to Index