Skip to content

feat(Units): parameterise Dimension and its unit twin over a basis (Stacked on #1445) #1447

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jstoobysmith merged 2 commits into from
Jul 22, 2026
Merged

feat(Units): parameterise Dimension and its unit twin over a basis (Stacked on #1445) #1447

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
de9d6a2
feat(Units): parameterise Dimension and its unit twin over a basis
NicolasRouquette Jul 19, 2026
d4c7056
refactor(Units): rename to LTMCTDimensionBase, add ISQ reference and …
NicolasRouquette Jul 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions Physlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
32 changes: 16 additions & 16 deletions Physlib/Units/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
/-!
Expand Down Expand Up @@ -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 : ℝ) *
Expand All @@ -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 : ℝ) *
Expand All @@ -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]

Expand All @@ -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 : ℝ)) *
Expand All @@ -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
Expand All @@ -177,22 +177,22 @@ 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 ?_
use u1.dimScale u2 d⁻¹
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
Expand Down Expand Up @@ -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 : ℝ) *
Expand All @@ -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 : ℝ) *
Expand All @@ -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

Expand Down
Loading
Loading