def definition def or abbrev

`units_identity_prop`

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)

   8def units_identity_prop : Prop :=

proof body

Definition body.

   9  ∀ U : IndisputableMonolith.Constants.RSUnits, U.c * U.tau0 = U.ell0
  10

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

units_identity_holds in IndisputableMonolith.URCAdapters.UnitsIdentity decl_use

depends on (10)

Lean names referenced from this declaration's body.

tau0 in IndisputableMonolith.Compat.Constants decl_use
ell0 in IndisputableMonolith.Constants decl_use
RSUnits in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
ell0 in IndisputableMonolith.Constants.Derivation decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
U in IndisputableMonolith.Recognition decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use