  30
  31/-- Dimensional signature: [Length, Time, Mass] exponents.
  32    Used to track physical dimensions through calculations. -/
  33structure Dimension where
  34  L : ℤ  -- Length exponent
  35  T : ℤ  -- Time exponent
  36  M : ℤ  -- Mass exponent
  37  deriving DecidableEq
  38
  39/-! ## Fundamental Dimension Constants -/
  40
  41/-- Dimensionless quantity: [L⁰T⁰M⁰] -/
  42def dim_one : Dimension := ⟨0, 0, 0⟩
  43
  44/-- Length dimension: [L¹T⁰M⁰] -/
  45def dim_L : Dimension := ⟨1, 0, 0⟩
  46
  47/-- Time dimension: [L⁰T¹M⁰] -/
  48def dim_T : Dimension := ⟨0, 1, 0⟩
  49
  50/-- Mass dimension: [L⁰T⁰M¹] -/
  51def dim_M : Dimension := ⟨0, 0, 1⟩
  52
  53/-! ## Physical Constant Dimensions -/
  54
  55/-- Speed of light dimension: [L¹T⁻¹M⁰] -/
  56def dim_c : Dimension := ⟨1, -1, 0⟩
  57
  58/-- Reduced Planck constant dimension: [L²T⁻¹M¹] -/
  59def dim_hbar : Dimension := ⟨2, -1, 1⟩
  60
  61/-- Gravitational constant dimension: [L³T⁻²M⁻¹] -/
  62def dim_G : Dimension := ⟨3, -2, -1⟩
  63

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.