structure
definition
def or abbrev
PositiveDimensionedQuantity
show as:
view Lean formalization →
formal statement (Lean)
99structure PositiveDimensionedQuantity extends DimensionedQuantity where
100 value_pos : 0 < value
101
102/-- Multiplication of dimensioned quantities. -/
103noncomputable def DimensionedQuantity.mul (q1 q2 : DimensionedQuantity) : DimensionedQuantity :=
proof body
Definition body.
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. -/