PhysLean Documentation

PhysLean.Units.Area

Area #

In this module we define the dimensionful type corresponding to an area. We define specific insances of areas, such as square meters, square feet, etc.

source
@[reducible, inline]
abbrev DimArea :
Type

The type of areas in the absence of a choice of unit.

Equations
Instances For

    Basic areas #

    source
    noncomputable def DimArea.squareMeter :
    DimArea

    The dimensional area corresponding to 1 square meter.

    Equations
    Instances For
      source
      noncomputable def DimArea.squareFoot :
      DimArea

      The dimensional area corresponding to 1 square foot.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def DimArea.squareMile :
        DimArea

        The dimensional area corresponding to 1 square mile.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def DimArea.are :
          DimArea

          The dimensional area corresponding to 1 are (100 square meters).

          Equations
          Instances For
            source
            noncomputable def DimArea.hectare :
            DimArea

            The dimensional area corresponding to 1 hectare (10,000 square meters).

            Equations
            Instances For
              source
              noncomputable def DimArea.acre :
              DimArea

              The dimensional area corresponding to 1 acre (1/640 square miles).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Area in SI units #

                source
                @[simp]
                theorem DimArea.squareMeter_in_SI :
                ↑squareMeter UnitChoices.SI = 1
                source
                @[simp]
                theorem DimArea.squareFoot_in_SI :
                ↑squareFoot UnitChoices.SI = 9290304e-8
                source
                @[simp]
                theorem DimArea.squareMile_in_SI :
                ↑squareMile UnitChoices.SI = 2589988.110336
                source
                @[simp]
                theorem DimArea.are_in_SI :
                ↑are UnitChoices.SI = 100
                source
                @[simp]
                theorem DimArea.hectare_in_SI :
                ↑hectare UnitChoices.SI = 10000
                source
                @[simp]
                theorem DimArea.acre_in_SI :
                ↑acre UnitChoices.SI = 4046.8564224

                ## Relations between areas

                source
                theorem DimArea.acre_eq_mul_squareFeet :
                acre = 43560 • squareFoot

                One acre is exactly 43560 square feet.