abbrev definition def or abbrev

`ZCharge`

show as: view Lean formalization →

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)

 208abbrev ZCharge := Quantity ZUnit

proof body

Definition body.

 209
 210end RSNative
 211end Measurement
 212end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.

Measurement in IndisputableMonolith.Data.Import decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
Quantity in IndisputableMonolith.Measurement.RSNative.Core decl_use
ZUnit in IndisputableMonolith.Measurement.RSNative.Core decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use