No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
167structure Quantity (U : Type) where
168 val : ℝ
169
170instance (U : Type) : CoeTC (Quantity U) ℝ := ⟨Quantity.val⟩
proof body
Definition body.
171
172namespace Quantity
173
174instance (U : Type) : Zero (Quantity U) := ⟨⟨0⟩⟩
175instance (U : Type) : Add (Quantity U) := ⟨fun a b => ⟨a.val + b.val⟩⟩
176instance (U : Type) : Sub (Quantity U) := ⟨fun a b => ⟨a.val - b.val⟩⟩
177instance (U : Type) : Neg (Quantity U) := ⟨fun a => ⟨-a.val⟩⟩
178instance (U : Type) : SMul ℝ (Quantity U) := ⟨fun r a => ⟨r * a.val⟩⟩
179
used by (14)
From the project-wide theorem graph. These declarations reference this one in their body.
-
Act
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Coh
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Meaning
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Qualia
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Skew
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Tick
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
val_add
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
val_neg
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
val_smul
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
val_sub
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
val_zero
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Voxel
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
ZCharge
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
depends on (2)
Lean names referenced from this declaration's body.
-
U
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
U
in IndisputableMonolith.Recognition
decl_use