27.4. The algebraic Remarks as kind-laws: physical chemistry built from the other parts🔗

The molar quantities of ISO 80000-9 are defined as quotients by the amount of substance — molar mass is m/n (9-4), molar volume V/n (9-5), the amount concentration n/V (9-12.1), molality n/m (9-15), the molar energies U/n (9-6.1) — composing Part-9 kinds out of ISO 80000-3 (volume), -4 (mass), and -5 (energy) kinds and the mole. Each is specified as an R12 kind-law.

Theorem27.4.1

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Molar mass is mass / amount of substance — a verified construction (item 9-4). A molar mass built as the quotient of a mass by an amount of substance carries its quotient certificate by construction, over the ℝ carrier, and canonicity makes the certificate determine the quantity. The companion molarMass_dim_from_mass_amount shows the result is a mass because the mole is dimension one. Uses the quotient kind-law.

Lean code for Theorem27.4.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part9/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part9.DefiningRelations.molarMassOf_isQuotient
  (m :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part4.mass.kind LTMCTDimensionBase)
      ℝ)
  (n :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part9.amountOfSubstance.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsQuotient
    PropertyKindCalculus.Iso80000.Part9.DefiningRelations.molarMass_quot_mass_amount
    (PropertyKindCalculus.Iso80000.Part9.DefiningRelations.molarMassOf m
      n)
    m n

theorem PropertyKindCalculus.Iso80000.Part9.DefiningRelations.molarMassOf_isQuotient
  (m :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part4.mass.kind
        LTMCTDimensionBase)
      ℝ)
  (n :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part9.amountOfSubstance.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsQuotient
    PropertyKindCalculus.Iso80000.Part9.DefiningRelations.molarMass_quot_mass_amount
    (PropertyKindCalculus.Iso80000.Part9.DefiningRelations.molarMassOf
      m n)
    m n

The constructed molar mass satisfies the quotient certificate by construction.

Proof for Theorem 27.4.1

uses 0

molarMassOf m n := Quantity.div molarMass_quot_mass_amount m n, and molarMassOf_isQuotient is rfl; molarMass_certificate_canonical is eq_div_of_isQuotient. The same family gives amountConcentrationOf (= n/V) and the cross-part kind-laws molarVolume_quot_volume_amount, molarInternalEnergy_quot_energy_amount, and molality_quot_amount_mass, crossing to ISO 80000-3/-4/-5.