diff --git a/Physlib.lean b/Physlib.lean
index 981f36e36..d8ac6620a 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -495,7 +495,12 @@ public import Physlib.Units.Basic
 public import Physlib.Units.Dimension
 public import Physlib.Units.Examples
 public import Physlib.Units.FDeriv
+public import Physlib.Units.ISQBridge
+public import Physlib.Units.ISQDimensionBase
 public import Physlib.Units.Integral
+public import Physlib.Units.LTMCTDimensionBase
+public import Physlib.Units.ParametricDimensionExamples
+public import Physlib.Units.ParametricUnits
 public import Physlib.Units.UnitDependent
 public import Physlib.Units.WithDim.Area
 public import Physlib.Units.WithDim.Basic
diff --git a/Physlib/Units/Basic.lean b/Physlib/Units/Basic.lean
index b604f276d..de70511e2 100644
--- a/Physlib/Units/Basic.lean
+++ b/Physlib/Units/Basic.lean
@@ -10,7 +10,7 @@ public import Physlib.SpaceAndTime.Space.LengthUnit
 public import Physlib.ClassicalMechanics.Mass.MassUnit
 public import Physlib.Electromagnetism.Charge.ChargeUnit
 public import Physlib.Thermodynamics.Temperature.TemperatureUnits
-public import Physlib.Units.Dimension
+public import Physlib.Units.LTMCTDimensionBase
 public import Physlib.Meta.TODO.Basic
 public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 /-!
@@ -98,7 +98,7 @@ namespace UnitChoices
 /-- Given two choices of units `u1` and `u2` and a dimension `d`, the
   element of `ℝ≥0` corresponding to the scaling (by definition) of a quantity of dimension `d`
   when changing from units `u1` to `u2`. -/
-noncomputable def dimScale (u1 u2 : UnitChoices) :Dimension →* ℝ≥0 where
+noncomputable def dimScale (u1 u2 : UnitChoices) :Dimension LTMCTDimensionBase →* ℝ≥0 where
   toFun d :=
     (u1.length / u2.length) ^ (d.length : ℝ) *
     (u1.time / u2.time) ^ (d.time : ℝ) *
@@ -115,7 +115,7 @@ noncomputable def dimScale (u1 u2 : UnitChoices) :Dimension →* ℝ≥0 where
     all_goals
       simp
 
-lemma dimScale_apply (u1 u2 : UnitChoices) (d : Dimension) :
+lemma dimScale_apply (u1 u2 : UnitChoices) (d : Dimension LTMCTDimensionBase) :
     dimScale u1 u2 d =
       (u1.length / u2.length) ^ (d.length : ℝ) *
       (u1.time / u2.time) ^ (d.time : ℝ) *
@@ -124,7 +124,7 @@ lemma dimScale_apply (u1 u2 : UnitChoices) (d : Dimension) :
       (u1.temperature / u2.temperature) ^ (d.temperature : ℝ) := rfl
 
 @[simp]
-lemma dimScale_self (u : UnitChoices) (d : Dimension) :
+lemma dimScale_self (u : UnitChoices) (d : Dimension LTMCTDimensionBase) :
     dimScale u u d = 1 := by
   simp [dimScale]
 
@@ -133,7 +133,7 @@ lemma dimScale_one (u1 u2 : UnitChoices) :
     dimScale u1 u2 1 = 1 := by
   simp [dimScale]
 
-lemma dimScale_transitive (u1 u2 u3 : UnitChoices) (d : Dimension) :
+lemma dimScale_transitive (u1 u2 u3 : UnitChoices) (d : Dimension LTMCTDimensionBase) :
     dimScale u1 u2 d * dimScale u2 u3 d = dimScale u1 u3 d := by
   simp [dimScale]
   trans ((u1.length / u2.length) ^ (d.length : ℝ) * (u2.length / u3.length) ^ (d.length : ℝ)) *
@@ -151,23 +151,23 @@ lemma dimScale_transitive (u1 u2 u3 : UnitChoices) (d : Dimension) :
   field_simp
 
 @[simp]
-lemma dimScale_mul_symm (u1 u2 : UnitChoices) (d : Dimension) :
+lemma dimScale_mul_symm (u1 u2 : UnitChoices) (d : Dimension LTMCTDimensionBase) :
     dimScale u1 u2 d * dimScale u2 u1 d = 1 := by
   rw [dimScale_transitive, dimScale_self]
 
 @[simp]
-lemma dimScale_coe_mul_symm (u1 u2 : UnitChoices) (d : Dimension) :
+lemma dimScale_coe_mul_symm (u1 u2 : UnitChoices) (d : Dimension LTMCTDimensionBase) :
     (toReal (dimScale u1 u2 d)) * (toReal (dimScale u2 u1 d)) = 1 := by
   trans toReal (dimScale u1 u2 d * dimScale u2 u1 d)
   · rw [NNReal.coe_mul]
   simp
 
 @[simp]
-lemma dimScale_ne_zero (u1 u2 : UnitChoices) (d : Dimension) :
+lemma dimScale_ne_zero (u1 u2 : UnitChoices) (d : Dimension LTMCTDimensionBase) :
     dimScale u1 u2 d ≠ 0 := by
   simp [dimScale]
 
-lemma dimScale_symm (u1 u2 : UnitChoices) (d : Dimension) :
+lemma dimScale_symm (u1 u2 : UnitChoices) (d : Dimension LTMCTDimensionBase) :
     dimScale u1 u2 d = (dimScale u2 u1 d)⁻¹ := by
   simp only [dimScale_apply, mul_inv]
   congr
@@ -177,14 +177,14 @@ lemma dimScale_symm (u1 u2 : UnitChoices) (d : Dimension) :
   · rw [ChargeUnit.div_symm, inv_rpow]
   · rw [TemperatureUnit.div_symm, inv_rpow]
 
-lemma dimScale_of_inv_eq_swap (u1 u2 : UnitChoices) (d : Dimension) :
+lemma dimScale_of_inv_eq_swap (u1 u2 : UnitChoices) (d : Dimension LTMCTDimensionBase) :
     dimScale u1 u2 d⁻¹ = dimScale u2 u1 d := by
   simp only [map_inv]
   conv_rhs => rw[dimScale_symm]
 
 @[simp]
-lemma smul_dimScale_injective {M : Type} [MulAction ℝ≥0 M] (u1 u2 : UnitChoices) (d : Dimension)
-    (m1 m2 : M) :
+lemma smul_dimScale_injective {M : Type} [MulAction ℝ≥0 M] (u1 u2 : UnitChoices)
+    (d : Dimension LTMCTDimensionBase) (m1 m2 : M) :
     (u1.dimScale u2 d) • m1 = (u1.dimScale u2 d) • m2 ↔ m1 = m2:= by
   refine IsUnit.smul_left_cancel ?_
   refine isUnit_iff_exists_inv.mpr ?_
@@ -192,7 +192,7 @@ lemma smul_dimScale_injective {M : Type} [MulAction ℝ≥0 M] (u1 u2 : UnitChoi
   simp
 
 @[simp]
-lemma dimScale_pos (u1 u2 : UnitChoices) (d : Dimension) :
+lemma dimScale_pos (u1 u2 : UnitChoices) (d : Dimension LTMCTDimensionBase) :
     0 < (dimScale u1 u2 d) := by
   apply lt_of_le_of_ne
   · simp
@@ -241,7 +241,7 @@ noncomputable def SIPrimed : UnitChoices where
   temperature := TemperatureUnit.scale 11 TemperatureUnit.kelvin
 
 @[simp]
-lemma dimScale_SI_SIPrimed (d : Dimension) :
+lemma dimScale_SI_SIPrimed (d : Dimension LTMCTDimensionBase) :
     dimScale SI SIPrimed d =
       (2⁻¹ : ℝ≥0) ^ (d.length : ℝ) *
       (3⁻¹ : ℝ≥0) ^ (d.time : ℝ) *
@@ -252,7 +252,7 @@ lemma dimScale_SI_SIPrimed (d : Dimension) :
   rfl
 
 @[simp]
-lemma dimScale_SIPrimed_SI (d : Dimension) :
+lemma dimScale_SIPrimed_SI (d : Dimension LTMCTDimensionBase) :
     dimScale SIPrimed SI d =
       (2 : ℝ≥0) ^ (d.length : ℝ) *
       (3 : ℝ≥0) ^ (d.time : ℝ) *
@@ -279,7 +279,7 @@ Dimensions are assigned to types with the following type-classes
   associated with the type `M`. -/
 class HasDim (M : Type) where
   /-- The dimension associated with a type `M`. -/
-  d : Dimension
+  d : Dimension LTMCTDimensionBase
 
 alias dim := HasDim.d
 
diff --git a/Physlib/Units/Dimension.lean b/Physlib/Units/Dimension.lean
index 3b59e8a3b..202d09123 100644
--- a/Physlib/Units/Dimension.lean
+++ b/Physlib/Units/Dimension.lean
@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Mathlib.Analysis.Normed.Field.Lemmas
+public import Mathlib.Tactic.DeriveFintype
 /-!
 
 # Dimension
@@ -13,6 +14,21 @@ public import Mathlib.Analysis.Normed.Field.Lemmas
 In this module we define the type `Dimension` which carries the dimension
 of a physical quantity.
 
+A `Dimension B` is parameterised by a *basis* `B` of base dimensions: it assigns a
+rational `exponent` to each base dimension `b : B`. The parameterisation is purely in
+the dimensional *algebra*: `Dimension B` is a `CommGroup` for every `B`
+(multiplication adds exponents, inversion negates them), so quantities can be typed by
+dimensions over any basis. The commutative-group and `ℚ`-power structure, decidable
+equality (`DecidableEq`), the base vectors `single b`, and the change-of-basis map
+`extend` are all generic in `B`.
+
+PhysLib's default basis is `LTMCTDimensionBase` — length, time, mass, charge,
+temperature — whose projections and named generators (`L𝓭`, `T𝓭`, …) live in
+`Physlib.Units.LTMCTDimensionBase`. It is *charge*-based with five generators, so it
+is **not** the SI/ISQ base-quantity set; the ISQ set is `ISQDimensionBase`, and other
+systems (Gaussian–CGS, natural units, …) are equally expressible as `Dimension B` for
+a suitable basis `B`.
+
 -/
 
 @[expose] public section
@@ -25,214 +41,172 @@ open NNReal
 
 -/
 
-/-- The foundational dimensions.
-  Defined in the order ⟨length, time, mass, charge, temperature⟩ -/
-structure Dimension where
-  /-- The length dimension. -/
-  length : ℚ
-  /-- The time dimension. -/
-  time : ℚ
-  /-- The mass dimension. -/
-  mass : ℚ
-  /-- The charge dimension. -/
-  charge : ℚ
-  /-- The temperature dimension. -/
-  temperature : ℚ
+/-- A dimension over a basis `B` of base dimensions: a rational `exponent` for each
+  base dimension `b : B`. PhysLib's default basis is `LTMCTDimensionBase`. -/
+structure Dimension (B : Type) where
+  /-- The exponent of each base dimension. -/
+  exponent : B → ℚ
 
 namespace Dimension
 
+variable {B : Type}
+
 @[ext]
-lemma ext {d1 d2 : Dimension}
-    (h1 : d1.length = d2.length)
-    (h2 : d1.time = d2.time)
-    (h3 : d1.mass = d2.mass)
-    (h4 : d1.charge = d2.charge)
-    (h5 : d1.temperature = d2.temperature) :
-    d1 = d2 := by
+lemma ext {d1 d2 : Dimension B} (h : ∀ b, d1.exponent b = d2.exponent b) : d1 = d2 := by
   cases d1
   cases d2
   congr
+  funext b
+  exact h b
 
-instance : Mul Dimension where
-  mul d1 d2 := ⟨d1.length + d2.length,
-    d1.time + d2.time,
-    d1.mass + d2.mass,
-    d1.charge + d2.charge,
-    d1.temperature + d2.temperature⟩
-
-@[simp]
-lemma time_mul (d1 d2 : Dimension) :
-    (d1 * d2).time = d1.time + d2.time := rfl
-
-@[simp]
-lemma length_mul (d1 d2 : Dimension) :
-    (d1 * d2).length = d1.length + d2.length := rfl
-
-@[simp]
-lemma mass_mul (d1 d2 : Dimension) :
-    (d1 * d2).mass = d1.mass + d2.mass := rfl
-
-@[simp]
-lemma charge_mul (d1 d2 : Dimension) :
-    (d1 * d2).charge = d1.charge + d2.charge := rfl
-
-@[simp]
-lemma temperature_mul (d1 d2 : Dimension) :
-    (d1 * d2).temperature = d1.temperature + d2.temperature := rfl
-
-instance : One Dimension where
-  one := ⟨0, 0, 0, 0, 0⟩
-
-@[simp]
-lemma one_length : (1 : Dimension).length = 0 := rfl
-@[simp]
-lemma one_time : (1 : Dimension).time = 0 := rfl
+instance : Mul (Dimension B) where
+  mul d1 d2 := ⟨fun b => d1.exponent b + d2.exponent b⟩
 
 @[simp]
-lemma one_mass : (1 : Dimension).mass = 0 := rfl
+lemma mul_exponent (d1 d2 : Dimension B) (b : B) :
+    (d1 * d2).exponent b = d1.exponent b + d2.exponent b := rfl
 
-@[simp]
-lemma one_charge : (1 : Dimension).charge = 0 := rfl
+instance : One (Dimension B) where
+  one := ⟨fun _ => 0⟩
 
 @[simp]
-lemma one_temperature : (1 : Dimension).temperature = 0 := rfl
+lemma one_exponent (b : B) : (1 : Dimension B).exponent b = 0 := rfl
 
-instance : CommGroup Dimension where
+instance : CommGroup (Dimension B) where
   mul_assoc a b c := by
-    ext
-    all_goals
-      simp only [length_mul, time_mul, mass_mul, charge_mul, temperature_mul]
-      ring
+    ext x
+    simp [add_assoc]
   one_mul a := by
-    ext
-    all_goals
-      simp
+    ext x
+    simp
   mul_one a := by
-    ext
-    all_goals
-      simp
-  inv d := ⟨-d.length, -d.time, -d.mass, -d.charge, -d.temperature⟩
+    ext x
+    simp
+  inv d := ⟨fun b => -d.exponent b⟩
   inv_mul_cancel a := by
-    ext
-    all_goals simp
+    ext x
+    simp
   mul_comm a b := by
-    ext
-    all_goals
-      simp only [length_mul, time_mul, mass_mul, charge_mul, temperature_mul]
-      ring
-
-@[simp]
-lemma inv_length (d : Dimension) : d⁻¹.length = -d.length := rfl
-
-@[simp]
-lemma inv_time (d : Dimension) : d⁻¹.time = -d.time := rfl
-
-@[simp]
-lemma inv_mass (d : Dimension) : d⁻¹.mass = -d.mass := rfl
-
-@[simp]
-lemma inv_charge (d : Dimension) : d⁻¹.charge = -d.charge := rfl
-
-@[simp]
-lemma inv_temperature (d : Dimension) : d⁻¹.temperature = -d.temperature := rfl
-
-@[simp]
-lemma div_length (d1 d2 : Dimension) : (d1 / d2).length = d1.length - d2.length := by
-  simp [div_eq_mul_inv, sub_eq_add_neg]
-
-@[simp]
-lemma div_time (d1 d2 : Dimension) : (d1 / d2).time = d1.time - d2.time := by
-  simp [div_eq_mul_inv, sub_eq_add_neg]
-
-@[simp]
-lemma div_mass (d1 d2 : Dimension) : (d1 / d2).mass = d1.mass - d2.mass := by
-  simp [div_eq_mul_inv, sub_eq_add_neg]
+    ext x
+    simp [add_comm]
 
 @[simp]
-lemma div_charge (d1 d2 : Dimension) : (d1 / d2).charge = d1.charge - d2.charge := by
-  simp [div_eq_mul_inv, sub_eq_add_neg]
+lemma inv_exponent (d : Dimension B) (b : B) : d⁻¹.exponent b = -d.exponent b := rfl
 
 @[simp]
-lemma div_temperature (d1 d2 : Dimension) :
-    (d1 / d2).temperature = d1.temperature - d2.temperature := by
+lemma div_exponent (d1 d2 : Dimension B) (b : B) :
+    (d1 / d2).exponent b = d1.exponent b - d2.exponent b := by
   simp [div_eq_mul_inv, sub_eq_add_neg]
 
 @[simp]
-lemma npow_length (d : Dimension) (n : ℕ) : (d ^ n).length = n • d.length := by
-  induction n with
-  | zero => simp
-  | succ n ih => rw [pow_succ, length_mul, ih, succ_nsmul]
-
-@[simp]
-lemma npow_time (d : Dimension) (n : ℕ) : (d ^ n).time = n • d.time := by
-  induction n with
-  | zero => simp
-  | succ n ih => rw [pow_succ, time_mul, ih, succ_nsmul]
-
-@[simp]
-lemma npow_mass (d : Dimension) (n : ℕ) : (d ^ n).mass = n • d.mass := by
-  induction n with
-  | zero => simp
-  | succ n ih => rw [pow_succ, mass_mul, ih, succ_nsmul]
-
-@[simp]
-lemma npow_charge (d : Dimension) (n : ℕ) : (d ^ n).charge = n • d.charge := by
-  induction n with
-  | zero => simp
-  | succ n ih => rw [pow_succ, charge_mul, ih, succ_nsmul]
-
-@[simp]
-lemma npow_temperature (d : Dimension) (n : ℕ) : (d ^ n).temperature = n • d.temperature := by
+lemma npow_exponent (d : Dimension B) (n : ℕ) (b : B) :
+    (d ^ n).exponent b = n • d.exponent b := by
   induction n with
   | zero => simp
-  | succ n ih => rw [pow_succ, temperature_mul, ih, succ_nsmul]
-
-instance : Pow Dimension ℚ where
-  pow d n := ⟨d.length * n, d.time * n, d.mass * n, d.charge * n, d.temperature * n⟩
+  | succ n ih => rw [pow_succ, mul_exponent, ih, succ_nsmul]
 
-/-- The dimension corresponding to length. -/
-def L𝓭 : Dimension := ⟨1, 0, 0, 0, 0⟩
-
-@[simp]
-lemma L𝓭_length : L𝓭.length = 1 := by rfl
+instance : Pow (Dimension B) ℚ where
+  pow d q := ⟨fun b => d.exponent b * q⟩
 
 @[simp]
-lemma L𝓭_time : L𝓭.time = 0 := by rfl
+lemma qpow_exponent (d : Dimension B) (q : ℚ) (b : B) :
+    (d ^ q).exponent b = d.exponent b * q := rfl
 
-@[simp]
-lemma L𝓭_mass : L𝓭.mass = 0 := by rfl
+/-- Decidable equality of dimensions over a finite basis `B`. -/
+instance [Fintype B] : DecidableEq (Dimension B) := fun d1 d2 =>
+  decidable_of_iff (∀ b, d1.exponent b = d2.exponent b)
+    ⟨fun h => Dimension.ext h, fun h _ => h ▸ rfl⟩
 
-@[simp]
-lemma L𝓭_charge : L𝓭.charge = 0 := by rfl
+/-- The base-dimension vector for `b : B`: exponent `1` at `b`, `0` elsewhere. This
+  is the generic analogue of the named generators `L𝓭`, `T𝓭`, … -/
+def single [DecidableEq B] (b : B) : Dimension B := ⟨Pi.single b 1⟩
 
 @[simp]
-lemma L𝓭_temperature : L𝓭.temperature = 0 := by rfl
+lemma single_exponent [DecidableEq B] (b b' : B) :
+    (single b).exponent b' = if b' = b then 1 else 0 := by
+  simp only [single, Pi.single_apply]
 
-/-- The dimension corresponding to time. -/
-def T𝓭 : Dimension := ⟨0, 1, 0, 0, 0⟩
+/-- Change of basis along a map `f : B → B'` of base dimensions: reindex a dimension
+  over `B` into one over `B'` by placing each exponent at its image. For an embedding
+  `f` (injective) this preserves every exponent (`extend_exponent_apply`), so a
+  dimension in one system re-expresses faithfully in an extending one. -/
+def extend {B' : Type} [Fintype B] [DecidableEq B'] (f : B → B') (d : Dimension B) :
+    Dimension B' :=
+  ⟨fun b' => ∑ b, if f b = b' then d.exponent b else 0⟩
 
 @[simp]
-lemma T𝓭_length : T𝓭.length = 0 := by rfl
+lemma extend_exponent_apply {B' : Type} [Fintype B] [DecidableEq B'] {f : B → B'}
+    (hf : Function.Injective f) (d : Dimension B) (b : B) :
+    (extend f d).exponent (f b) = d.exponent b := by
+  simp only [extend]
+  rw [Finset.sum_eq_single b (fun b'' _ hne => by simp [hf.ne hne]) (by simp)]
+  simp
 
-@[simp]
-lemma T𝓭_time : T𝓭.time = 1 := by rfl
+/-!
 
-@[simp]
-lemma T𝓭_mass : T𝓭.mass = 0 := by rfl
+## Dimension-preserving maps between bases
 
-@[simp]
-lemma T𝓭_charge : T𝓭.charge = 0 := by rfl
+A cross-basis map of dimensions is only admissible if it preserves the dimensional
+*algebra*. We record the two truth-preserving directions as bundled data:
 
-@[simp]
-lemma T𝓭_temperature : T𝓭.temperature = 0 := by rfl
+* an `Embedding B B'` is an **injective** `MonoidHom (Dimension B) (Dimension B')` — a
+  faithful, dimension-preserving inclusion of one basis into another; and
+* a `Projection B' B` is a **surjective** `MonoidHom (Dimension B') (Dimension B)` — a
+  truth-preserving *reduction* of a richer basis onto a coarser one.
 
-/-- The dimension corresponding to mass. -/
-def M𝓭 : Dimension := ⟨0, 0, 1, 0, 0⟩
+Being a `MonoidHom` is what makes either map dimension-preserving (it respects
+products, inverses and rational powers); the injectivity / surjectivity side condition
+distinguishes the two directions. Cross-basis dimension maps should be produced as one
+of these, so that dimension-preservation holds by construction — a bare relabelling
+that sends a base dimension to an inequivalent one is *not* expressible as either.
 
-/-- The dimension corresponding to charge. -/
-def C𝓭 : Dimension := ⟨0, 0, 0, 1, 0⟩
+-/
 
-/-- The dimension corresponding to temperature. -/
-def Θ𝓭 : Dimension := ⟨0, 0, 0, 0, 1⟩
+/-- `extend f` packaged as a monoid homomorphism of dimensions. -/
+def extendHom {B' : Type} [Fintype B] [DecidableEq B'] (f : B → B') :
+    Dimension B →* Dimension B' where
+  toFun := extend f
+  map_one' := by ext b'; simp [extend]
+  map_mul' d1 d2 := by
+    ext b'
+    simp only [extend, mul_exponent]
+    rw [← Finset.sum_add_distrib]
+    refine Finset.sum_congr rfl fun b _ => ?_
+    split_ifs <;> simp
+
+/-- A **dimension embedding** `B ↪ B'`: an injective monoid homomorphism of
+  dimensions. As a `MonoidHom` it is dimension-preserving (it respects products,
+  inverses and rational powers); injectivity makes it a faithful inclusion of the basis
+  `B` into `B'`. Cross-basis dimension injections are produced as `Embedding`s so that
+  dimension-preservation holds by construction. -/
+structure Embedding (B B' : Type) where
+  /-- The underlying dimension-preserving homomorphism. -/
+  toHom : Dimension B →* Dimension B'
+  /-- The homomorphism is injective (a faithful embedding). -/
+  inj : Function.Injective toHom
+
+/-- A **dimension projection** `B' ↠ B`: a surjective monoid homomorphism of
+  dimensions. As a `MonoidHom` it is truth-preserving, but it is lossy — it reduces a
+  richer basis `B'` onto a coarser basis `B`, collapsing the base dimensions that `B`
+  does not track. -/
+structure Projection (B' B : Type) where
+  /-- The underlying dimension-preserving homomorphism. -/
+  toHom : Dimension B' →* Dimension B
+  /-- The homomorphism is surjective (the reduction hits every dimension of `B`). -/
+  surj : Function.Surjective toHom
+
+/-- An injective *basis* map `f : B → B'` induces a dimension embedding, via `extend`.
+  This is the label-level case: it sends each base dimension of `B` to a base dimension
+  of `B'`, so it is automatically dimension-preserving and faithful. -/
+def Embedding.ofBasis {B B' : Type} [Fintype B] [DecidableEq B']
+    (f : B → B') (hf : Function.Injective f) : Embedding B B' where
+  toHom := extendHom f
+  inj := by
+    intro d1 d2 h
+    ext b
+    have h2 : (extendHom f d1).exponent (f b) = (extendHom f d2).exponent (f b) := by
+      rw [h]
+    simpa only [extendHom, MonoidHom.coe_mk, OneHom.coe_mk, extend_exponent_apply hf]
+      using h2
 
 end Dimension
diff --git a/Physlib/Units/ISQBridge.lean b/Physlib/Units/ISQBridge.lean
new file mode 100644
index 000000000..1f15d5926
--- /dev/null
+++ b/Physlib/Units/ISQBridge.lean
@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 Nicolas Rouquette. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nicolas Rouquette
+-/
+module
+
+public import Physlib.Units.LTMCTDimensionBase
+public import Physlib.Units.ISQDimensionBase
+/-!
+
+# Bridging PhysLib's default basis and the ISQ basis
+
+`LTMCTDimensionBase` (length, time, mass, charge, temperature) and `ISQDimensionBase`
+(the seven ISO/IEC 80000-1 base quantities) make different base/derived choices. This
+module relates them by the two truth-preserving directions of `Dimension.Embedding`
+and `Dimension.Projection`:
+
+* `ltmctToISQ : Dimension.Embedding LTMCTDimensionBase ISQDimensionBase` — the
+  dimension-preserving **inclusion** of PhysLib dimensions into ISQ dimensions. It
+  sends the charge generator to the *derived* ISQ charge `I · T` (`toISQHom_C𝓭`), so it
+  is faithful (`toISQHom_injective`) and physically correct, not a bare relabelling.
+* `isqToLTMCT : Dimension.Projection ISQDimensionBase LTMCTDimensionBase` — the
+  truth-preserving **reduction** of ISQ dimensions onto PhysLib's. It reads electric
+  current as charge/time and forgets amount of substance and luminous intensity (the
+  base quantities PhysLib does not track).
+
+The two fit together as a retraction, `isqToLTMCT ∘ ltmctToISQ = id`
+(`isqToLTMCT_comp_ltmctToISQ`): PhysLib's basis embeds faithfully into ISQ and is
+recovered exactly by the projection — but the reverse composite is *not* the identity,
+because amount of substance and luminous intensity cannot be recovered once dropped.
+That is the asymmetry: one can reduce ISQ to LTMCT, but not conjure the extra base
+quantities back without *adding* them.
+
+-/
+
+@[expose] public section
+
+namespace Dimension
+
+/-- The function underlying `toISQHom`: fix length, mass, time and temperature, and
+  send PhysLib's charge generator to the derived ISQ charge `I · T` (the current
+  exponent is the charge exponent, and the time exponent absorbs it). -/
+def toISQFun (d : Dimension LTMCTDimensionBase) : Dimension ISQDimensionBase :=
+  ⟨fun
+    | .length => d.exponent .length
+    | .mass => d.exponent .mass
+    | .time => d.exponent .time + d.exponent .charge
+    | .current => d.exponent .charge
+    | .temperature => d.exponent .temperature
+    | .amount => 0
+    | .luminousIntensity => 0⟩
+
+/-- The dimension-preserving embedding of PhysLib dimensions into the ISQ dimensions. -/
+def toISQHom : Dimension LTMCTDimensionBase →* Dimension ISQDimensionBase where
+  toFun := toISQFun
+  map_one' := by ext b; cases b <;> simp [toISQFun]
+  map_mul' d1 d2 := by
+    ext b
+    cases b <;> simp only [toISQFun, mul_exponent]
+    all_goals ring
+
+/-- `toISQHom` applied to a dimension is `toISQFun`. -/
+lemma toISQHom_apply (d : Dimension LTMCTDimensionBase) : toISQHom d = toISQFun d := rfl
+
+/-- The function underlying `fromISQHom`: fix length, mass and temperature, read
+  electric current as charge/time (the charge exponent is the current exponent, and the
+  time exponent subtracts it), and drop amount of substance and luminous intensity. -/
+def fromISQFun (d : Dimension ISQDimensionBase) : Dimension LTMCTDimensionBase :=
+  ⟨fun
+    | .length => d.exponent .length
+    | .time => d.exponent .time - d.exponent .current
+    | .mass => d.exponent .mass
+    | .charge => d.exponent .current
+    | .temperature => d.exponent .temperature⟩
+
+/-- The truth-preserving reduction of ISQ dimensions onto PhysLib's. -/
+def fromISQHom : Dimension ISQDimensionBase →* Dimension LTMCTDimensionBase where
+  toFun := fromISQFun
+  map_one' := by ext b; cases b <;> simp [fromISQFun]
+  map_mul' d1 d2 := by
+    ext b
+    cases b <;> simp only [fromISQFun, mul_exponent]
+    all_goals ring
+
+/-- `fromISQHom` applied to a dimension is `fromISQFun`. -/
+lemma fromISQHom_apply (d : Dimension ISQDimensionBase) : fromISQHom d = fromISQFun d := rfl
+
+/-- The projection recovers PhysLib's basis from its image under the embedding:
+  `fromISQHom ∘ toISQHom = id`. -/
+lemma fromISQHom_comp_toISQHom :
+    fromISQHom.comp toISQHom = MonoidHom.id (Dimension LTMCTDimensionBase) := by
+  refine MonoidHom.ext fun d => Dimension.ext fun b => ?_
+  cases b <;> simp only [MonoidHom.comp_apply, MonoidHom.id_apply, toISQHom_apply,
+    fromISQHom_apply, fromISQFun, toISQFun]
+  all_goals ring
+
+/-- `toISQHom` is injective: PhysLib dimensions include faithfully into ISQ. -/
+lemma toISQHom_injective : Function.Injective toISQHom := by
+  intro d1 d2 h
+  have key : ∀ b : ISQDimensionBase, (toISQFun d1).exponent b = (toISQFun d2).exponent b := by
+    intro b
+    have hb := congrArg (fun d => Dimension.exponent d b) h
+    simpa only [toISQHom_apply] using hb
+  ext b
+  cases b with
+  | length => simpa only [toISQFun] using key .length
+  | time =>
+      have ht := key .time
+      have hc := key .current
+      simp only [toISQFun] at ht hc
+      linarith
+  | mass => simpa only [toISQFun] using key .mass
+  | charge => simpa only [toISQFun] using key .current
+  | temperature => simpa only [toISQFun] using key .temperature
+
+/-- `fromISQHom` is surjective: every PhysLib dimension is the reduction of some ISQ
+  dimension (namely its own embedding). -/
+lemma fromISQHom_surjective : Function.Surjective fromISQHom := fun y =>
+  ⟨toISQHom y, by rw [← MonoidHom.comp_apply, fromISQHom_comp_toISQHom, MonoidHom.id_apply]⟩
+
+/-- PhysLib's dimensions embed into the ISQ dimensions (charge ↦ `I · T`). -/
+def ltmctToISQ : Embedding LTMCTDimensionBase ISQDimensionBase where
+  toHom := toISQHom
+  inj := toISQHom_injective
+
+/-- The ISQ dimensions project onto PhysLib's, reading current as charge/time and
+  forgetting amount of substance and luminous intensity. -/
+def isqToLTMCT : Projection ISQDimensionBase LTMCTDimensionBase where
+  toHom := fromISQHom
+  surj := fromISQHom_surjective
+
+/-- The projection is a retraction of the embedding: `isqToLTMCT ∘ ltmctToISQ = id`. So
+  PhysLib's basis embeds faithfully into ISQ and is recovered by the projection, but not
+  conversely — amount of substance and luminous intensity cannot be recovered. -/
+lemma isqToLTMCT_comp_ltmctToISQ :
+    isqToLTMCT.toHom.comp ltmctToISQ.toHom = MonoidHom.id (Dimension LTMCTDimensionBase) :=
+  fromISQHom_comp_toISQHom
+
+/-- The embedding is physically faithful on charge: PhysLib's charge generator `C𝓭`
+  maps to the *derived* ISQ charge `I · T`. -/
+lemma toISQHom_C𝓭 : toISQHom C𝓭 = ISQDimensionBase.charge := by
+  ext b
+  cases b <;> simp [toISQHom_apply, toISQFun, C𝓭, ofLTMCTDimensionBase,
+    ISQDimensionBase.charge, single_exponent]
+
+end Dimension
diff --git a/Physlib/Units/ISQDimensionBase.lean b/Physlib/Units/ISQDimensionBase.lean
new file mode 100644
index 000000000..8b5782cbe
--- /dev/null
+++ b/Physlib/Units/ISQDimensionBase.lean
@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Nicolas Rouquette. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nicolas Rouquette
+-/
+module
+
+public import Physlib.Units.Dimension
+/-!
+
+# The ISQ base quantities
+
+The International System of Quantities (ISQ), specified in ISO/IEC 80000-1 and
+described in the International Vocabulary of Metrology (VIM, 3rd edition,
+JCGM 200:2012), fixes seven mutually independent *base quantities*: length, mass,
+time, electric current, thermodynamic temperature, amount of substance, and
+luminous intensity.
+
+`ISQDimensionBase` is that seven-element basis, realised as an instantiation
+`Dimension ISQDimensionBase` of the parametric dimensional algebra. It differs from
+PhysLib's default `LTMCTDimensionBase` in two ways:
+
+* the electromagnetic base quantity is *electric current*, so electric charge is a
+  *derived* dimension (`Q = I · T`, `ISQDimensionBase.charge`); and
+* *amount of substance* and *luminous intensity* are additional independent base
+  quantities.
+
+## References
+
+* ISO/IEC 80000-1:2009, *Quantities and units — Part 1: General*.
+* JCGM 200:2012, *International vocabulary of metrology — Basic and general concepts
+  and associated terms (VIM, 3rd edition)*.
+
+-/
+
+@[expose] public section
+
+open Dimension
+
+/-- The seven ISQ base quantities (ISO/IEC 80000-1; VIM 3rd edition). Unlike
+  `LTMCTDimensionBase`, electric current is the electromagnetic base quantity (so
+  charge is derived), and amount of substance and luminous intensity are further
+  base quantities. -/
+inductive ISQDimensionBase where
+  /-- The length base quantity. -/
+  | length
+  /-- The mass base quantity. -/
+  | mass
+  /-- The time base quantity. -/
+  | time
+  /-- The electric-current base quantity. -/
+  | current
+  /-- The thermodynamic-temperature base quantity. -/
+  | temperature
+  /-- The amount-of-substance base quantity. -/
+  | amount
+  /-- The luminous-intensity base quantity. -/
+  | luminousIntensity
+deriving DecidableEq, Fintype
+
+namespace ISQDimensionBase
+
+/-- The ISQ has seven base quantities. -/
+lemma card_eq_seven : Fintype.card ISQDimensionBase = 7 := by decide
+
+/-- Electric charge is a *derived* dimension in the ISQ: `Q = I · T`. -/
+def charge : Dimension ISQDimensionBase := single .current * single .time
+
+/-- The derived charge dimension has electric-current exponent `1`. -/
+lemma charge_exponent_current : charge.exponent .current = 1 := by
+  simp [charge, single_exponent]
+
+/-- The derived charge dimension has time exponent `1`. -/
+lemma charge_exponent_time : charge.exponent .time = 1 := by
+  simp [charge, single_exponent]
+
+/-- The derived charge dimension has mass exponent `0`. -/
+lemma charge_exponent_mass : charge.exponent .mass = 0 := by
+  simp [charge, single_exponent]
+
+/-- Amount of substance is an independent base dimension (absent from
+  `LTMCTDimensionBase`). -/
+lemma single_amount_ne_one : single (.amount : ISQDimensionBase) ≠ 1 := by
+  intro h
+  have := congrArg (fun d => Dimension.exponent d .amount) h
+  simp [single_exponent] at this
+
+/-- Luminous intensity is an independent base dimension (absent from
+  `LTMCTDimensionBase`). -/
+lemma single_luminousIntensity_ne_one :
+    single (.luminousIntensity : ISQDimensionBase) ≠ 1 := by
+  intro h
+  have := congrArg (fun d => Dimension.exponent d .luminousIntensity) h
+  simp [single_exponent] at this
+
+end ISQDimensionBase
diff --git a/Physlib/Units/Integral.lean b/Physlib/Units/Integral.lean
index ae28cffb6..14f3bb7ec 100644
--- a/Physlib/Units/Integral.lean
+++ b/Physlib/Units/Integral.lean
@@ -69,7 +69,7 @@ fun (μ : DimSet (MeasureTheory.Measure M) d)
     (f : DimSet (M → G) (CarriesDimension.d G * d⁻¹)) ↦ ∫ x, f.1 x ∂μ.1
 ```
   is dimensionally correct. -/
-lemma integral_isDimensionallyCorrect (d : Dimension) :
+lemma integral_isDimensionallyCorrect (d : Dimension LTMCTDimensionBase) :
     IsDimensionallyCorrect (fun (μ : DimSet (MeasureTheory.Measure M) d)
       (f : DimSet (M → G) (dim G * d⁻¹)) ↦ ∫ x, f.1 x ∂μ.1) := by
   intro u1 u2
diff --git a/Physlib/Units/LTMCTDimensionBase.lean b/Physlib/Units/LTMCTDimensionBase.lean
new file mode 100644
index 000000000..fc297a07f
--- /dev/null
+++ b/Physlib/Units/LTMCTDimensionBase.lean
@@ -0,0 +1,261 @@
+/-
+Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import Physlib.Units.Dimension
+/-!
+
+# PhysLib's default dimension basis
+
+`LTMCTDimensionBase` is PhysLib's default basis of base dimensions — length, time,
+mass, charge and temperature. `Dimension LTMCTDimensionBase` is the familiar
+five-exponent dimension, and this module provides the concrete API on top of the
+generic `Dimension B`:
+
+* the `.length`, `.time`, `.mass`, `.charge`, `.temperature` exponent projections;
+* the `ofLTMCTDimensionBase` constructor from five exponents; and
+* the named generators `L𝓭`, `T𝓭`, `M𝓭`, `C𝓭`, `Θ𝓭`, shown to be the generic
+  `single` base vectors.
+
+This basis is *charge*-based with five generators, so it is deliberately **not** the
+SI/ISQ base-quantity set (which takes electric current as base and adds amount of
+substance and luminous intensity); see `ISQDimensionBase`.
+
+-/
+
+@[expose] public section
+
+/-- PhysLib's default basis of base dimensions — `length`, `time`, `mass`,
+  `charge`, `temperature`. Note this is *charge*-based, so it is not the SI/ISQ
+  base-quantity set; see `Dimension`. -/
+inductive LTMCTDimensionBase where
+  /-- The length base dimension. -/
+  | length
+  /-- The time base dimension. -/
+  | time
+  /-- The mass base dimension. -/
+  | mass
+  /-- The charge base dimension. -/
+  | charge
+  /-- The temperature base dimension. -/
+  | temperature
+deriving DecidableEq, Fintype
+
+namespace Dimension
+
+/-!
+
+## The LTMCTDimensionBase projections
+
+The five base-dimension exponents of a `Dimension LTMCTDimensionBase`, provided so that
+the familiar `.length`, `.time`, `.mass`, `.charge`, `.temperature` API is available.
+
+-/
+
+/-- The length exponent of a `LTMCTDimensionBase` dimension. -/
+def length (d : Dimension LTMCTDimensionBase) : ℚ := d.exponent .length
+/-- The time exponent of a `LTMCTDimensionBase` dimension. -/
+def time (d : Dimension LTMCTDimensionBase) : ℚ := d.exponent .time
+/-- The mass exponent of a `LTMCTDimensionBase` dimension. -/
+def mass (d : Dimension LTMCTDimensionBase) : ℚ := d.exponent .mass
+/-- The charge exponent of a `LTMCTDimensionBase` dimension. -/
+def charge (d : Dimension LTMCTDimensionBase) : ℚ := d.exponent .charge
+/-- The temperature exponent of a `LTMCTDimensionBase` dimension. -/
+def temperature (d : Dimension LTMCTDimensionBase) : ℚ := d.exponent .temperature
+
+/-- Build a `LTMCTDimensionBase` dimension from its five exponents, in the order
+  `⟨length, time, mass, charge, temperature⟩`. -/
+def ofLTMCTDimensionBase (length time mass charge temperature : ℚ) : Dimension LTMCTDimensionBase :=
+  ⟨fun
+    | .length => length
+    | .time => time
+    | .mass => mass
+    | .charge => charge
+    | .temperature => temperature⟩
+
+@[simp]
+lemma ofLTMCTDimensionBase_length (l t m c θ : ℚ) :
+    (ofLTMCTDimensionBase l t m c θ).length = l := rfl
+
+@[simp]
+lemma ofLTMCTDimensionBase_time (l t m c θ : ℚ) :
+    (ofLTMCTDimensionBase l t m c θ).time = t := rfl
+
+@[simp]
+lemma ofLTMCTDimensionBase_mass (l t m c θ : ℚ) :
+    (ofLTMCTDimensionBase l t m c θ).mass = m := rfl
+
+@[simp]
+lemma ofLTMCTDimensionBase_charge (l t m c θ : ℚ) :
+    (ofLTMCTDimensionBase l t m c θ).charge = c := rfl
+
+@[simp]
+lemma ofLTMCTDimensionBase_temperature (l t m c θ : ℚ) :
+    (ofLTMCTDimensionBase l t m c θ).temperature = θ := rfl
+
+@[simp]
+lemma time_mul (d1 d2 : Dimension LTMCTDimensionBase) :
+    (d1 * d2).time = d1.time + d2.time := rfl
+
+@[simp]
+lemma length_mul (d1 d2 : Dimension LTMCTDimensionBase) :
+    (d1 * d2).length = d1.length + d2.length := rfl
+
+@[simp]
+lemma mass_mul (d1 d2 : Dimension LTMCTDimensionBase) :
+    (d1 * d2).mass = d1.mass + d2.mass := rfl
+
+@[simp]
+lemma charge_mul (d1 d2 : Dimension LTMCTDimensionBase) :
+    (d1 * d2).charge = d1.charge + d2.charge := rfl
+
+@[simp]
+lemma temperature_mul (d1 d2 : Dimension LTMCTDimensionBase) :
+    (d1 * d2).temperature = d1.temperature + d2.temperature := rfl
+
+@[simp]
+lemma one_length : (1 : Dimension LTMCTDimensionBase).length = 0 := rfl
+@[simp]
+lemma one_time : (1 : Dimension LTMCTDimensionBase).time = 0 := rfl
+
+@[simp]
+lemma one_mass : (1 : Dimension LTMCTDimensionBase).mass = 0 := rfl
+
+@[simp]
+lemma one_charge : (1 : Dimension LTMCTDimensionBase).charge = 0 := rfl
+
+@[simp]
+lemma one_temperature : (1 : Dimension LTMCTDimensionBase).temperature = 0 := rfl
+
+@[simp]
+lemma inv_length (d : Dimension LTMCTDimensionBase) : d⁻¹.length = -d.length := rfl
+
+@[simp]
+lemma inv_time (d : Dimension LTMCTDimensionBase) : d⁻¹.time = -d.time := rfl
+
+@[simp]
+lemma inv_mass (d : Dimension LTMCTDimensionBase) : d⁻¹.mass = -d.mass := rfl
+
+@[simp]
+lemma inv_charge (d : Dimension LTMCTDimensionBase) : d⁻¹.charge = -d.charge := rfl
+
+@[simp]
+lemma inv_temperature (d : Dimension LTMCTDimensionBase) : d⁻¹.temperature = -d.temperature := rfl
+
+@[simp]
+lemma div_length (d1 d2 : Dimension LTMCTDimensionBase) :
+    (d1 / d2).length = d1.length - d2.length := by
+  simp only [length, div_exponent]
+
+@[simp]
+lemma div_time (d1 d2 : Dimension LTMCTDimensionBase) : (d1 / d2).time = d1.time - d2.time := by
+  simp only [time, div_exponent]
+
+@[simp]
+lemma div_mass (d1 d2 : Dimension LTMCTDimensionBase) : (d1 / d2).mass = d1.mass - d2.mass := by
+  simp only [mass, div_exponent]
+
+@[simp]
+lemma div_charge (d1 d2 : Dimension LTMCTDimensionBase) :
+    (d1 / d2).charge = d1.charge - d2.charge := by
+  simp only [charge, div_exponent]
+
+@[simp]
+lemma div_temperature (d1 d2 : Dimension LTMCTDimensionBase) :
+    (d1 / d2).temperature = d1.temperature - d2.temperature := by
+  simp only [temperature, div_exponent]
+
+@[simp]
+lemma npow_length (d : Dimension LTMCTDimensionBase) (n : ℕ) : (d ^ n).length = n • d.length := by
+  simp only [length, npow_exponent]
+
+@[simp]
+lemma npow_time (d : Dimension LTMCTDimensionBase) (n : ℕ) : (d ^ n).time = n • d.time := by
+  simp only [time, npow_exponent]
+
+@[simp]
+lemma npow_mass (d : Dimension LTMCTDimensionBase) (n : ℕ) : (d ^ n).mass = n • d.mass := by
+  simp only [mass, npow_exponent]
+
+@[simp]
+lemma npow_charge (d : Dimension LTMCTDimensionBase) (n : ℕ) : (d ^ n).charge = n • d.charge := by
+  simp only [charge, npow_exponent]
+
+@[simp]
+lemma npow_temperature (d : Dimension LTMCTDimensionBase) (n : ℕ) :
+    (d ^ n).temperature = n • d.temperature := by
+  simp only [temperature, npow_exponent]
+
+/-- The dimension corresponding to length. -/
+def L𝓭 : Dimension LTMCTDimensionBase := ofLTMCTDimensionBase 1 0 0 0 0
+
+@[simp]
+lemma L𝓭_length : L𝓭.length = 1 := by rfl
+
+@[simp]
+lemma L𝓭_time : L𝓭.time = 0 := by rfl
+
+@[simp]
+lemma L𝓭_mass : L𝓭.mass = 0 := by rfl
+
+@[simp]
+lemma L𝓭_charge : L𝓭.charge = 0 := by rfl
+
+@[simp]
+lemma L𝓭_temperature : L𝓭.temperature = 0 := by rfl
+
+/-- The dimension corresponding to time. -/
+def T𝓭 : Dimension LTMCTDimensionBase := ofLTMCTDimensionBase 0 1 0 0 0
+
+@[simp]
+lemma T𝓭_length : T𝓭.length = 0 := by rfl
+
+@[simp]
+lemma T𝓭_time : T𝓭.time = 1 := by rfl
+
+@[simp]
+lemma T𝓭_mass : T𝓭.mass = 0 := by rfl
+
+@[simp]
+lemma T𝓭_charge : T𝓭.charge = 0 := by rfl
+
+@[simp]
+lemma T𝓭_temperature : T𝓭.temperature = 0 := by rfl
+
+/-- The dimension corresponding to mass. -/
+def M𝓭 : Dimension LTMCTDimensionBase := ofLTMCTDimensionBase 0 0 1 0 0
+
+/-- The dimension corresponding to charge. -/
+def C𝓭 : Dimension LTMCTDimensionBase := ofLTMCTDimensionBase 0 0 0 1 0
+
+/-- The dimension corresponding to temperature. -/
+def Θ𝓭 : Dimension LTMCTDimensionBase := ofLTMCTDimensionBase 0 0 0 0 1
+
+/-!
+
+## The named generators are the base vectors
+
+Each named generator `L𝓭`, `T𝓭`, … is the generic `single` base vector at the
+corresponding base dimension, exhibiting them as instances of the basis-generic API.
+
+-/
+
+lemma L𝓭_eq_single : L𝓭 = single .length := by
+  ext b; cases b <;> simp [L𝓭, ofLTMCTDimensionBase, single_exponent]
+
+lemma T𝓭_eq_single : T𝓭 = single .time := by
+  ext b; cases b <;> simp [T𝓭, ofLTMCTDimensionBase, single_exponent]
+
+lemma M𝓭_eq_single : M𝓭 = single .mass := by
+  ext b; cases b <;> simp [M𝓭, ofLTMCTDimensionBase, single_exponent]
+
+lemma C𝓭_eq_single : C𝓭 = single .charge := by
+  ext b; cases b <;> simp [C𝓭, ofLTMCTDimensionBase, single_exponent]
+
+lemma Θ𝓭_eq_single : Θ𝓭 = single .temperature := by
+  ext b; cases b <;> simp [Θ𝓭, ofLTMCTDimensionBase, single_exponent]
+
+end Dimension
diff --git a/Physlib/Units/ParametricDimensionExamples.lean b/Physlib/Units/ParametricDimensionExamples.lean
new file mode 100644
index 000000000..c6f8fd296
--- /dev/null
+++ b/Physlib/Units/ParametricDimensionExamples.lean
@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2026 Nicolas Rouquette. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nicolas Rouquette
+-/
+module
+
+public import Physlib.Units.WithDim.Basic
+/-!
+
+# Examples: parametric dimensions and comparing dimensioned quantities
+
+`Dimension B` is parameterised by a basis `B` of base dimensions. This module
+illustrates two consequences.
+
+## Comparing a length with a velocity times a time
+
+A recurring question is how to compare a quantity of dimension `length` with a
+product of a quantity of dimension `length / time` and a quantity of dimension
+`time`. The two dimensions are *equal*, but this equality is a **group
+cancellation law** on the rational exponents — it holds *propositionally*, never
+*definitionally*:
+
+* `(L𝓭 / T𝓭) * T𝓭 = L𝓭` cannot be closed by `rfl`: cancellation is not a
+  reduction rule.
+* nor by `decide`: the exponents are rational, so the kernel has nothing to
+  evaluate.
+
+Consequently `WithDim ((L𝓭 / T𝓭) * T𝓭) ℝ` and `WithDim L𝓭 ℝ` are genuinely
+different types, and a bare `x = v * t` is a type error. The bridge is
+`WithDim.cast`, whose default argument discharges the propositional dimension
+equality automatically, so the comparison is a one-liner. This is not a
+limitation of the representation: no representation of `Dimension` makes the
+equality definitional, so a cast on a proven equality is the correct idiom.
+
+## A non-standard basis
+
+Because `Dimension` is parametric, the same dimensional algebra and the same
+`cast`-based comparison are available over *any* basis — not just the physical
+`LTMCTDimensionBase`. The unit-scaling layer (`UnitChoices`, `dimScale`) is not needed
+for either the algebra or the comparison, so neither is referenced here.
+
+This module is illustrative and should not be imported by other modules.
+
+-/
+
+@[expose] public section
+
+open Dimension
+
+namespace ParametricDimensionExamples
+
+/-- The dimension equality `(length / time) · time = length` holds
+propositionally, by cancellation of the rational exponents. -/
+example : (L𝓭 / T𝓭) * T𝓭 = L𝓭 := by ext; simp
+
+/-- The dimensions are equal, but the two `WithDim` *types* are not
+definitionally equal, so `WithDim.cast` bridges them. Its default argument proves
+`(L𝓭 / T𝓭) * T𝓭 = L𝓭` with no manual proof. -/
+noncomputable example (v : WithDim (L𝓭 / T𝓭) ℝ) (t : WithDim T𝓭 ℝ) : WithDim L𝓭 ℝ :=
+  (v * t).cast
+
+/-- The end-to-end comparison: a length equals a velocity times a time, once the
+product is cast to the length dimension. -/
+example (x : WithDim L𝓭 ℝ) (v : WithDim (L𝓭 / T𝓭) ℝ) (t : WithDim T𝓭 ℝ) : Prop :=
+  x = (v * t).cast
+
+/-!
+## The same comparison over a non-standard basis
+
+A basis with two base dimensions of its own — `bit` and `symbol` — that
+`LTMCTDimensionBase` does not have. Nothing in the standard units system is involved.
+-/
+
+/-- A basis of information-theoretic base dimensions. -/
+inductive Info
+  /-- The information base dimension (bits). -/
+  | bit
+  /-- The symbol base dimension. -/
+  | symbol
+
+/-- The `bit` base dimension. -/
+def bitDim : Dimension Info := ⟨fun | .bit => 1 | .symbol => 0⟩
+
+/-- The `symbol` base dimension. -/
+def symbolDim : Dimension Info := ⟨fun | .bit => 0 | .symbol => 1⟩
+
+/-- Cancellation works identically over the non-standard basis. -/
+example : (bitDim / symbolDim) * symbolDim = bitDim := by ext; simp
+
+/-- And so does the `cast`-based comparison: an information content equals an
+information rate (`bit / symbol`) times a number of symbols. -/
+example (x : WithDim bitDim ℝ) (r : WithDim (bitDim / symbolDim) ℝ)
+    (n : WithDim symbolDim ℝ) : Prop :=
+  x = (r * n).cast
+
+end ParametricDimensionExamples
diff --git a/Physlib/Units/ParametricUnits.lean b/Physlib/Units/ParametricUnits.lean
new file mode 100644
index 000000000..cda0ff5ce
--- /dev/null
+++ b/Physlib/Units/ParametricUnits.lean
@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2026 Nicolas Rouquette. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nicolas Rouquette
+-/
+module
+
+public import Physlib.Units.Basic
+/-!
+
+# The unit side, parametrised in the same basis
+
+The dimension basis is parametric (`Dimension B`), but the *unit* side of the
+bridge is hardwired in parallel: `UnitChoices` has five named unit fields and
+`UnitChoices.dimScale` folds over exactly those five. This module provides the
+generic twin, parametrised in the same basis `B`.
+
+Every PhysLib base unit (`LengthUnit`, `TimeUnit`, …) is, structurally, a positive
+real (`{ val : ℝ // 0 < val }`); the typed names carry no extra algebraic content.
+So a unit choice over a basis `B` is a positive real per base dimension, and the
+scaling homomorphism folds the per-base unit ratio over `B`:
+
+* `UnitScale B` — a positive-real magnitude for each `b : B`.
+* `UnitScale.dimScale : UnitScale B → UnitScale B → Dimension B →* ℝ≥0` — the
+  `MonoidHom` `d ↦ ∏ b, (u₁ b / u₂ b) ^ d.exponent b`, generic in `B`.
+
+The current five-field `UnitChoices.dimScale` is the `LTMCTDimensionBase` instance of this
+fold, written out by hand; `UnitChoices.toScale` exhibits the correspondence.
+
+-/
+
+@[expose] public section
+
+open NNReal
+open scoped BigOperators
+
+/-- A choice of unit for each base dimension of `B`: a positive-real magnitude per
+  base. This is the basis-generic form of `UnitChoices`. -/
+structure UnitScale (B : Type) where
+  /-- The positive-real magnitude of the chosen unit at each base dimension. -/
+  scale : B → ℝ≥0
+  /-- Each chosen unit has a positive magnitude. -/
+  scale_pos : ∀ b, 0 < scale b
+
+namespace UnitScale
+
+variable {B : Type}
+
+lemma ratio_ne_zero (u1 u2 : UnitScale B) (b : B) : u1.scale b / u2.scale b ≠ 0 :=
+  (div_pos (u1.scale_pos b) (u2.scale_pos b)).ne'
+
+/-- The dimension-scaling homomorphism, generic in the basis `B`: a quantity of
+  dimension `d` rescales by `∏ b, (u1 b / u2 b) ^ d.exponent b` when changing the
+  unit choice from `u1` to `u2`. This is the basis-generic form of
+  `UnitChoices.dimScale`. -/
+noncomputable def dimScale [Fintype B] (u1 u2 : UnitScale B) : Dimension B →* ℝ≥0 where
+  toFun d := ∏ b, (u1.scale b / u2.scale b) ^ (d.exponent b : ℝ)
+  map_one' := by simp
+  map_mul' d1 d2 := by
+    simp only [Dimension.mul_exponent, Rat.cast_add]
+    rw [← Finset.prod_mul_distrib]
+    exact Finset.prod_congr rfl fun b _ =>
+      NNReal.rpow_add (u1.ratio_ne_zero u2 b) _ _
+
+@[simp]
+lemma dimScale_self [Fintype B] (u : UnitScale B) (d : Dimension B) :
+    dimScale u u d = 1 := by
+  simp only [dimScale, MonoidHom.coe_mk, OneHom.coe_mk]
+  refine Finset.prod_eq_one fun b _ => ?_
+  rw [div_self (u.scale_pos b).ne', NNReal.one_rpow]
+
+@[simp]
+lemma dimScale_one [Fintype B] (u1 u2 : UnitScale B) :
+    dimScale u1 u2 1 = 1 := map_one _
+
+/-- The scaling is transitive (a cocycle in the unit choices). -/
+lemma dimScale_transitive [Fintype B] (u1 u2 u3 : UnitScale B) (d : Dimension B) :
+    dimScale u1 u2 d * dimScale u2 u3 d = dimScale u1 u3 d := by
+  simp only [dimScale, MonoidHom.coe_mk, OneHom.coe_mk, ← Finset.prod_mul_distrib]
+  refine Finset.prod_congr rfl fun b _ => ?_
+  rw [← NNReal.mul_rpow]
+  congr 1
+  rw [div_mul_div_comm, mul_comm (u2.scale b), mul_div_mul_right _ _ (u2.scale_pos b).ne']
+
+end UnitScale
+
+/-!
+## The current five-field `UnitChoices` is the `LTMCTDimensionBase` instance
+
+`UnitChoices.toScale` reads the five typed units as a `UnitScale LTMCTDimensionBase`,
+exhibiting the existing bespoke `dimScale` as the `LTMCTDimensionBase` case of the generic
+fold.
+-/
+
+namespace UnitChoices
+
+/-- Read a five-field `UnitChoices` as a `UnitScale` over `LTMCTDimensionBase`. -/
+noncomputable def toScale (u : UnitChoices) : UnitScale LTMCTDimensionBase where
+  scale
+    | .length => ⟨u.length.val, u.length.val_pos.le⟩
+    | .time => ⟨u.time.val, u.time.val_pos.le⟩
+    | .mass => ⟨u.mass.val, u.mass.val_pos.le⟩
+    | .charge => ⟨u.charge.val, u.charge.val_pos.le⟩
+    | .temperature => ⟨u.temperature.val, u.temperature.val_pos.le⟩
+  scale_pos b := by
+    cases b
+    · exact NNReal.coe_pos.mp u.length.val_pos
+    · exact NNReal.coe_pos.mp u.time.val_pos
+    · exact NNReal.coe_pos.mp u.mass.val_pos
+    · exact NNReal.coe_pos.mp u.charge.val_pos
+    · exact NNReal.coe_pos.mp u.temperature.val_pos
+
+end UnitChoices
diff --git a/Physlib/Units/UnitDependent.lean b/Physlib/Units/UnitDependent.lean
index 8784f3a45..336ed69ce 100644
--- a/Physlib/Units/UnitDependent.lean
+++ b/Physlib/Units/UnitDependent.lean
@@ -197,7 +197,7 @@ lemma UnitChoices.scaleUnit_apply_fst (u1 u2 : UnitChoices) :
     ChargeUnit.div_eq_val, TemperatureUnit.div_eq_val, toReal]
 
 @[simp]
-lemma UnitChoices.dimScale_scaleUnit {u1 u2 u : UnitChoices} (d : Dimension) :
+lemma UnitChoices.dimScale_scaleUnit {u1 u2 u : UnitChoices} (d : Dimension LTMCTDimensionBase) :
     u.dimScale (scaleUnit u1 u2 u) d = u1.dimScale u2 d := by
   simp [dimScale, scaleUnit]
   simp [LengthUnit.div_eq_val, TimeUnit.div_eq_val, MassUnit.div_eq_val, ChargeUnit.div_eq_val,
@@ -472,10 +472,11 @@ lemma DMul.hMul_scaleUnit {M1 M2 M3 : Type} [CarriesDimension M1] [CarriesDimens
 
 /-- Given a type `M` that depends on units, e.g. the function type `M1 → M2` between two types
   carrying a dimension, the subtype of `M` which scales according to the dimension `d`. -/
-def DimSet (M : Type) [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension) : Set M :=
+def DimSet (M : Type) [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension LTMCTDimensionBase) :
+    Set M :=
   {m : M | ∀ u1 u2, scaleUnit u1 u2 m = (UnitChoices.dimScale u1 u2 d) • m}
 
-instance (M : Type) [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension) :
+instance (M : Type) [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension LTMCTDimensionBase) :
     MulAction ℝ≥0 (DimSet M d) where
   smul a f := ⟨a • f.1, fun u1 u2 => by
     rw [smul_comm, ← f.2]
@@ -489,14 +490,15 @@ instance (M : Type) [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension) :
     change (a * b) • f.1 = a • (b • f.1)
     rw [smul_smul]
 
-instance (M : Type) [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension) :
+instance (M : Type) [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension LTMCTDimensionBase) :
     CarriesDimension (DimSet M d) where
   d := d
 
 @[simp]
-lemma scaleUnit_dimSet_val {M : Type} [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension)
-    (m : DimSet M d) (u1 u2 : UnitChoices) :
+lemma scaleUnit_dimSet_val {M : Type} [MulAction ℝ≥0 M] [MulUnitDependent M]
+    (d : Dimension LTMCTDimensionBase) (m : DimSet M d) (u1 u2 : UnitChoices) :
     (scaleUnit u1 u2 m).1 = scaleUnit u1 u2 m.1 := (m.2 u1 u2).symm
 
-lemma DimSet.mem_iff {M : Type} [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension) (m : M) :
+lemma DimSet.mem_iff {M : Type} [MulAction ℝ≥0 M] [MulUnitDependent M]
+    (d : Dimension LTMCTDimensionBase) (m : M) :
     m ∈ DimSet M d ↔ ∀ u1 u2, scaleUnit u1 u2 m = (UnitChoices.dimScale u1 u2 d) • m := by rfl
diff --git a/Physlib/Units/WithDim/Basic.lean b/Physlib/Units/WithDim/Basic.lean
index 5f9687c67..501724194 100644
--- a/Physlib/Units/WithDim/Basic.lean
+++ b/Physlib/Units/WithDim/Basic.lean
@@ -12,6 +12,13 @@ public import Physlib.Units.UnitDependent
 
 WithDim is the type `M` which carrying the dimension `d`.
 
+The dimension `d : Dimension B` may be taken over any basis `B` of base dimensions.
+The *algebraic* structure of `WithDim d M` (its additive, order, scalar-action,
+multiplication, division and casting instances) is available for every basis `B`.
+The *unit-scaling* structure (`HasDim`, `DMul`, and the `scaleUnit` lemmas), which
+routes through `UnitChoices.dimScale`, is provided for the standard basis
+`LTMCTDimensionBase`.
+
 -/
 
 @[expose] public section
@@ -19,73 +26,74 @@ WithDim is the type `M` which carrying the dimension `d`.
 open NNReal
 
 /-- The type `M` carrying an instance of a dimension `d`. -/
-structure WithDim (d : Dimension) (M : Type) where
+structure WithDim {B : Type} (d : Dimension B) (M : Type) where
   /-- The underlying value of `M`. -/
   val : M
 
 namespace WithDim
 
 @[ext]
-lemma ext {d M} (x1 x2 : WithDim d M) (h : x1.val = x2.val) : x1 = x2 := by
+lemma ext {B : Type} {d : Dimension B} {M} (x1 x2 : WithDim d M) (h : x1.val = x2.val) :
+    x1 = x2 := by
   cases x1
   cases x2
   simp_all
 
-instance (d : Dimension) (M : Type) : HasDim (WithDim d M) where
+instance (d : Dimension LTMCTDimensionBase) (M : Type) : HasDim (WithDim d M) where
   d := d
 
 @[simp]
-lemma dim_apply (d : Dimension) (M : Type) :
+lemma dim_apply (d : Dimension LTMCTDimensionBase) (M : Type) :
     dim (WithDim d M) = d := rfl
 
 /-!
 ## Inherited instances
 -/
 
-instance (d : Dimension) (M : Type) [Inhabited M] : Inhabited (WithDim d M) where
+instance {B : Type} (d : Dimension B) (M : Type) [Inhabited M] : Inhabited (WithDim d M) where
   default := ⟨default⟩
 
-instance (d : Dimension) (M : Type) [Zero M] : Zero (WithDim d M) where
+instance {B : Type} (d : Dimension B) (M : Type) [Zero M] : Zero (WithDim d M) where
   zero := ⟨0⟩
 
 @[simp]
-lemma val_zero {d : Dimension} {M : Type} [Zero M] :
+lemma val_zero {B : Type} {d : Dimension B} {M : Type} [Zero M] :
     (0 : WithDim d M).val = 0 := rfl
 
-instance (d : Dimension) (M : Type) [Add M] : Add (WithDim d M) where
+instance {B : Type} (d : Dimension B) (M : Type) [Add M] : Add (WithDim d M) where
   add m1 m2 := ⟨m1.val + m2.val⟩
 
 @[simp]
-lemma val_add {d : Dimension} {M : Type} [Add M] (m1 m2 : WithDim d M) :
+lemma val_add {B : Type} {d : Dimension B} {M : Type} [Add M] (m1 m2 : WithDim d M) :
     (m1 + m2).val = m1.val + m2.val := rfl
 
-instance (d : Dimension) (M : Type) [Neg M] : Neg (WithDim d M) where
+instance {B : Type} (d : Dimension B) (M : Type) [Neg M] : Neg (WithDim d M) where
   neg m := ⟨-m.val⟩
 
 @[simp]
-lemma val_neg {d : Dimension} {M : Type} [Neg M] (m : WithDim d M) :
+lemma val_neg {B : Type} {d : Dimension B} {M : Type} [Neg M] (m : WithDim d M) :
     (-m).val = -m.val := rfl
 
-instance (d : Dimension) (M : Type) [Sub M] : Sub (WithDim d M) where
+instance {B : Type} (d : Dimension B) (M : Type) [Sub M] : Sub (WithDim d M) where
   sub m1 m2 := ⟨m1.val - m2.val⟩
 
 @[simp]
-lemma val_sub {d : Dimension} {M : Type} [Sub M] (m1 m2 : WithDim d M) :
+lemma val_sub {B : Type} {d : Dimension B} {M : Type} [Sub M] (m1 m2 : WithDim d M) :
     (m1 - m2).val = m1.val - m2.val := rfl
 
-instance (d : Dimension) (M : Type) [AddSemigroup M] :
+instance {B : Type} (d : Dimension B) (M : Type) [AddSemigroup M] :
     AddSemigroup (WithDim d M) where
   add_assoc m1 m2 m3 := by
     ext
     simp [add_assoc]
 
-instance (d : Dimension) (M : Type) [AddCommSemigroup M] :
+instance {B : Type} (d : Dimension B) (M : Type) [AddCommSemigroup M] :
     AddCommSemigroup (WithDim d M) where
   add_comm m1 m2 := by
     ext
     simp [add_comm]
 
-instance (d : Dimension) (M : Type) [AddMonoid M] :
+instance {B : Type} (d : Dimension B) (M : Type) [AddMonoid M] :
     AddMonoid (WithDim d M) where
   zero_add m := by
     ext
@@ -95,13 +103,13 @@ instance (d : Dimension) (M : Type) [AddMonoid M] :
     simp [add_zero]
   nsmul := nsmulRec
 
-instance (d : Dimension) (M : Type) [AddCommMonoid M] :
+instance {B : Type} (d : Dimension B) (M : Type) [AddCommMonoid M] :
     AddCommMonoid (WithDim d M) where
   add_comm m1 m2 := by
     ext
     simp [add_comm]
 
-instance (d : Dimension) (M : Type) [AddGroup M] :
+instance {B : Type} (d : Dimension B) (M : Type) [AddGroup M] :
     AddGroup (WithDim d M) where
   sub_eq_add_neg m1 m2 := by
     ext
@@ -111,27 +119,27 @@ instance (d : Dimension) (M : Type) [AddGroup M] :
     simp [neg_add_cancel]
   zsmul := zsmulRec
 
-instance (d : Dimension) (M : Type) [AddCommGroup M] :
+instance {B : Type} (d : Dimension B) (M : Type) [AddCommGroup M] :
     AddCommGroup (WithDim d M) where
   add_comm m1 m2 := by
     ext
     simp [add_comm]
 
-instance (d : Dimension) (M : Type) [LE M] : LE (WithDim d M) where
+instance {B : Type} (d : Dimension B) (M : Type) [LE M] : LE (WithDim d M) where
   le m1 m2 := m1.val ≤ m2.val
 
 @[simp]
-lemma le_def {d : Dimension} {M : Type} [LE M] (m1 m2 : WithDim d M) :
+lemma le_def {B : Type} {d : Dimension B} {M : Type} [LE M] (m1 m2 : WithDim d M) :
     m1 ≤ m2 ↔ m1.val ≤ m2.val := Iff.rfl
 
-instance (d : Dimension) (M : Type) [LT M] : LT (WithDim d M) where
+instance {B : Type} (d : Dimension B) (M : Type) [LT M] : LT (WithDim d M) where
   lt m1 m2 := m1.val < m2.val
 
 @[simp]
-lemma lt_def {d : Dimension} {M : Type} [LT M] (m1 m2 : WithDim d M) :
+lemma lt_def {B : Type} {d : Dimension B} {M : Type} [LT M] (m1 m2 : WithDim d M) :
     m1 < m2 ↔ m1.val < m2.val := Iff.rfl
 
-instance (d : Dimension) (M : Type) [Preorder M] :
+instance {B : Type} (d : Dimension B) (M : Type) [Preorder M] :
     Preorder (WithDim d M) where
   le_refl m := by
     exact le_refl m.val
@@ -142,13 +150,14 @@ instance (d : Dimension) (M : Type) [Preorder M] :
     change m1.val < m2.val ↔ m1.val ≤ m2.val ∧ ¬ m2.val ≤ m1.val
     exact lt_iff_le_not_ge
 
-instance (d : Dimension) (M : Type) [PartialOrder M] :
+instance {B : Type} (d : Dimension B) (M : Type) [PartialOrder M] :
     PartialOrder (WithDim d M) where
   le_antisymm m1 m2 h12 h21 := by
     ext
     exact le_antisymm h12 h21
 
-instance (d : Dimension) (M : Type) [MulAction ℝ≥0 M] : MulAction ℝ≥0 (WithDim d M) where
+instance {B : Type} (d : Dimension B) (M : Type) [MulAction ℝ≥0 M] :
+    MulAction ℝ≥0 (WithDim d M) where
   smul a m := ⟨a • m.val⟩
   one_smul m := ext _ _ (one_smul ℝ≥0 m.val)
   mul_smul a b m := by
@@ -156,17 +165,19 @@ instance (d : Dimension) (M : Type) [MulAction ℝ≥0 M] : MulAction ℝ≥0 (W
     exact mul_smul a b m.val
 
 @[simp]
-lemma smul_val {d : Dimension} {M : Type} [MulAction ℝ≥0 M] (a : ℝ≥0) (m : WithDim d M) :
+lemma smul_val {B : Type} {d : Dimension B} {M : Type} [MulAction ℝ≥0 M]
+    (a : ℝ≥0) (m : WithDim d M) :
     (a • m).val = a • m.val := rfl
 
-instance {d1 d2 : Dimension} :
+instance {B : Type} {d1 d2 : Dimension B} :
     HMul (WithDim d1 ℝ) (WithDim d2 ℝ) (WithDim (d1 * d2) ℝ) where
   hMul m1 m2 := ⟨m1.val * m2.val⟩
 
-lemma withDim_hMul_val {d1 d2 : Dimension} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) :
+lemma withDim_hMul_val {B : Type} {d1 d2 : Dimension B}
+    (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) :
     (m1 * m2).val = m1.val * m2.val := rfl
 
-instance {d1 d2 : Dimension} :
+instance {d1 d2 : Dimension LTMCTDimensionBase} :
     DMul (WithDim d1 ℝ) (WithDim d2 ℝ) (WithDim (d1 * d2) ℝ) where
   mul_dim m1 m2 := by
     intro u1 u2
@@ -181,32 +192,34 @@ instance {d1 d2 : Dimension} :
 open UnitDependent
 
 @[simp]
-lemma val_mul_eq_mul {d1 d2 : Dimension} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) :
+lemma val_mul_eq_mul {B : Type} {d1 d2 : Dimension B}
+    (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) :
     m1.val * m2.val = (m1 * m2).val := by
   simp only [withDim_hMul_val]
 
 @[simp]
-lemma val_pow_two_eq_mul {d1 : Dimension} (m1 : WithDim d1 ℝ) :
+lemma val_pow_two_eq_mul {B : Type} {d1 : Dimension B} (m1 : WithDim d1 ℝ) :
     m1.val ^ 2 = (m1 * m1).val := by
   rw [sq]
   rfl
 
 @[simp]
-lemma scaleUnit_val_eq_scaleUnit_val {d : Dimension} (M : Type) [MulAction ℝ≥0 M]
+lemma scaleUnit_val_eq_scaleUnit_val {d : Dimension LTMCTDimensionBase} (M : Type) [MulAction ℝ≥0 M]
     (u1 u2 : UnitChoices) (m1 m2 : WithDim d M) :
     (scaleUnit u1 u2 m1).val = (scaleUnit u1 u2 m2).val ↔ m1.val = m2.val := by
   rw [← WithDim.ext_iff]
   simp only [scaleUnit_injective]
   exact WithDim.ext_iff
 
-lemma scaleUnit_val_eq_scaleUnit_val_of_dim_eq {d1 d2 : Dimension} {M : Type} [MulAction ℝ≥0 M]
+lemma scaleUnit_val_eq_scaleUnit_val_of_dim_eq {d1 d2 : Dimension LTMCTDimensionBase} {M : Type}
+    [MulAction ℝ≥0 M]
     {u1 u2 : UnitChoices} {m1 : WithDim d1 M} {m2 : WithDim d2 M}
     (h : d1 = d2 := by ext <;> {simp; try ring}) :
     (scaleUnit u1 u2 m1).val = (scaleUnit u1 u2 m2).val ↔ m1.val = m2.val := by
   subst h
   simp
 
-lemma scaleUnit_val {d : Dimension} (M : Type) [MulAction ℝ≥0 M]
+lemma scaleUnit_val {d : Dimension LTMCTDimensionBase} (M : Type) [MulAction ℝ≥0 M]
     (u1 u2 : UnitChoices) (m1 : WithDim d M) :
     (scaleUnit u1 u2 m1).val = u1.dimScale u2 d • m1.val := rfl
 
@@ -216,16 +229,16 @@ lemma scaleUnit_val {d : Dimension} (M : Type) [MulAction ℝ≥0 M]
 
 -/
 
-noncomputable instance (d1 d2 : Dimension) :
+noncomputable instance {B : Type} (d1 d2 : Dimension B) :
     HDiv (WithDim d1 ℝ) (WithDim d2 ℝ) (WithDim (d1 * d2⁻¹) ℝ) where
   hDiv m1 m2 := ⟨m1.val / m2.val⟩
 
 @[simp]
-lemma val_div_val {d1 d2 : Dimension} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) :
+lemma val_div_val {B : Type} {d1 d2 : Dimension B} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) :
     (m1.val / m2.val) = (m1 / m2).val := rfl
 
 @[simp]
-lemma div_scaleUnit {d1 d2 : Dimension} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ)
+lemma div_scaleUnit {d1 d2 : Dimension LTMCTDimensionBase} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ)
     (u1 u2 : UnitChoices) :
     (scaleUnit u1 u2 m1) / (scaleUnit u1 u2 m2) = scaleUnit u1 u2 (m1 / m2) := by
   symm
@@ -239,8 +252,9 @@ lemma div_scaleUnit {d1 d2 : Dimension} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 
   exact div_mul_div_comm (↑((u1.dimScale u2) d1)) (↑((u1.dimScale u2) d2)) m1.val m2.val
 
 @[simp]
-lemma scaleUnit_dim_eq_zero {d : Dimension} (m : WithDim d ℝ) (u1 u2 : UnitChoices)
-    (h : d = 1 := by ext <;> {simp; try ring}) : scaleUnit u1 u2 m = m := by
+lemma scaleUnit_dim_eq_zero {d : Dimension LTMCTDimensionBase} (m : WithDim d ℝ)
+    (u1 u2 : UnitChoices) (h : d = 1 := by ext <;> {simp; try ring}) :
+    scaleUnit u1 u2 m = m := by
   subst h
   ext
   rw [scaleUnit_val]
@@ -253,15 +267,16 @@ lemma scaleUnit_dim_eq_zero {d : Dimension} (m : WithDim d ℝ) (u1 u2 : UnitCho
 set_option linter.unusedVariables false in
 /-- The casting from `WithDim d M` to `WithDim d2 M` when `d = d2`. -/
 @[nolint unusedArguments]
-def cast {d d2 : Dimension} {M : Type} (m : WithDim d M)
+def cast {B : Type} {d d2 : Dimension B} {M : Type} (m : WithDim d M)
     (h : d = d2 := by ext <;> {simp; try ring}) : WithDim d2 M := ⟨m.val⟩
 
 @[simp]
-lemma cast_refl {d : Dimension} {M : Type} (m : WithDim d M) :
+lemma cast_refl {B : Type} {d : Dimension B} {M : Type} (m : WithDim d M) :
     cast m rfl = m := rfl
 
 @[simp]
-lemma cast_scaleUnit {d d2 : Dimension} {M : Type} [MulAction ℝ≥0 M] (m : WithDim d M)
+lemma cast_scaleUnit {d d2 : Dimension LTMCTDimensionBase} {M : Type} [MulAction ℝ≥0 M]
+    (m : WithDim d M)
     (h : d = d2) (u1 u2 : UnitChoices) :
     cast (scaleUnit u1 u2 m) h = scaleUnit u1 u2 (cast m h) := by
   subst h