21.4. Standard prefixes: the centimetre as centi · metre🔗

A unit is rarely used alone — a length is reported in millimetres, kilometres, or centimetres, all the same kind as the metre but differing by a decimal factor. The VIM4 records this directly: §1.19 lists the SI prefixes (a factor 10ⁿ with a name and a symbol), §1.20 and §1.21 define a multiple and a submultiple of a unit, and §1.22 the conversion factor between two units of the same kind. So the centimetre is not an independent unit named "cm": it is the centi submultiple of the metre, and its symbol and its 10⁻² factor should follow from that, not be asserted by hand.

Definition21.4.1

groupuses 1used by 0✓L∃∀N

A prefixed unit is a decimal (SI, §1.19) or binary (IEC 80000-13) prefix applied to a base unit. It projects to a metrological unit of the same kind with the prefix symbol prepended ("c" ++ "m" = "cm"), and exposes its §1.22 conversion factor as the exponent and its §1.20/§1.21 status as a multiple or submultiple.

Lean code for Definition21.4.1●1 definition

structure(4 fields)defined in PropertyKindCalculus/UnitPrefix.lean

complete

structure PropertyKindCalculus.PrefixedUnit : Type

structure PropertyKindCalculus.PrefixedUnit : Type

**§1.20 / §1.21 — a prefixed unit.** A `MetrologicalUnit` formed by applying a
decimal (SI, §1.19) *or* binary (IEC 80000-13) prefix to a base unit: a multiple
(`exponent > 0`) or submultiple (`exponent < 0`) of the same kind. The provenance is
carried in *resolved* form — the numeric `radix` (`10` for an SI prefix, `2` for a
binary one), the power-of-radix `exponent`, and the prefix `symbol` — so that both
prefix families share one prefixed-unit and one conversion round-trip, and so
conversion can be gated to units of the *same radix* (`SameRadix`).

Fields

radix : ℕ

The numeric base of the prefix: `10` for an SI decimal prefix (§1.19), `2` for
an IEC 80000-13 binary prefix. The §1.22 conversion factor is `radix ^ exponent`.

exponent : ℤ

The power: `1` prefixed unit is `radix ^ exponent` base units (centi = `-2`,
kilo = `3`; kibi = `10` at radix `2`).

symbol : String

The prefix symbol, prepended to the base unit symbol (`"c"`, `"k"`, `"Ki"`).

base : PropertyKindCalculus.MetrologicalUnit

The base unit the prefix is applied to.

Proof for Definition 21.4.1

uses 0

Realized as structure SIPrefix (name, symbol, exponent : Int) with the full §1.19 table (and a sibling BinaryPrefix for IEC 80000-13), and structure PrefixedUnit (radix, exponent, symbol, base) with toUnit (the projection), conversionExponent, IsMultiple, and IsSubmultiple. Recording the resolved radix lets both prefix families share one prefixed unit; the projection preserves the kind, so toUnit_wellFormed and commensurable_base follow by reflexivity.

Theorem21.4.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

The centimetre is the centi submultiple of the metre, factor 10⁻². Its symbol "cm" and its conversion exponent -2 are checked computations from the prefix and the base, and it stays commensurable with the metre. Uses metrological units.

Lean code for Theorem21.4.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part3.lean

complete

theorem PropertyKindCalculus.Iso80000.Part3.centimetre_conversionExponent :
  PropertyKindCalculus.Iso80000.Part3.centimetrePrefixed.conversionExponent =
    -2

theorem PropertyKindCalculus.Iso80000.Part3.centimetre_conversionExponent :
  PropertyKindCalculus.Iso80000.Part3.centimetrePrefixed.conversionExponent =
    -2

The centimetre is a submultiple of the metre with conversion factor `10⁻²`.

Proof for Theorem 21.4.2

uses 0

centimetre is (metre.withPrefix SIPrefix.centi).toUnit. The facts centimetre_symbol = "cm", centimetre_conversionExponent = -2, centimetre_isSubmultiple, and centimetre_wellFormed are discharged by rfl / decide; metre_centimetre_commensurable holds because the prefix leaves the kind unchanged.