structure
definition
PositiveDimensionedQuantity
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Constants.Dimensions on GitHub at line 99.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
formal source
96 dim : Dimension
97
98/-- A positive dimensioned quantity (for physical constants). -/
99structure PositiveDimensionedQuantity extends DimensionedQuantity where
100 value_pos : 0 < value
101
102/-- Multiplication of dimensioned quantities. -/
103noncomputable def DimensionedQuantity.mul (q1 q2 : DimensionedQuantity) : DimensionedQuantity :=
104 ⟨q1.value * q2.value, ⟨q1.dim.L + q2.dim.L, q1.dim.T + q2.dim.T, q1.dim.M + q2.dim.M⟩⟩
105
106/-- Division of dimensioned quantities. -/
107noncomputable def DimensionedQuantity.div (q1 q2 : DimensionedQuantity) : DimensionedQuantity :=
108 ⟨q1.value / q2.value, ⟨q1.dim.L - q2.dim.L, q1.dim.T - q2.dim.T, q1.dim.M - q2.dim.M⟩⟩
109
110/-- Square root of a dimensioned quantity (for even dimension exponents). -/
111noncomputable def DimensionedQuantity.sqrt (q : DimensionedQuantity) : DimensionedQuantity :=
112 ⟨Real.sqrt q.value, ⟨q.dim.L / 2, q.dim.T / 2, q.dim.M / 2⟩⟩
113
114/-! ## Status Report -/
115
116/-- Summary of dimensional analysis module. -/
117def dimensions_status : String :=
118 "✓ Dimension structure [L, T, M] defined\n" ++
119 "✓ Physical constant dimensions (c, ℏ, G) specified\n" ++
120 "✓ Planck unit dimensions documented\n" ++
121 "✓ τ₀ dimension documented as [T]\n" ++
122 "✓ DimensionedQuantity algebra defined"
123
124#eval dimensions_status
125
126end Dimensions
127end Constants
128end IndisputableMonolith