structure definition def or abbrev

`U`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  95structure U where
  96  a : Unit
  97
  98/-- Recognition relation by structural equality -/

used by (40)

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

BerlyneInvertedUCert in IndisputableMonolith.Aesthetics.BerlyneInvertedU decl_use
aestheticCost_zero_at_optimum in IndisputableMonolith.Aesthetics.CulturalAestheticFromJCost decl_use
computeRatios in IndisputableMonolith.Certificates.UnitsKGate decl_use
AtomicTick in IndisputableMonolith.Chain decl_use
Chain in IndisputableMonolith.Chain decl_use
head in IndisputableMonolith.Chain decl_use
last in IndisputableMonolith.Chain decl_use
Ledger in IndisputableMonolith.Chain decl_use
phi in IndisputableMonolith.Chain decl_use
RecognitionStructure in IndisputableMonolith.Chain decl_use
co_highest_curie in IndisputableMonolith.Chemistry.Ferromagnetism decl_use
stonerCriterion in IndisputableMonolith.Chemistry.Ferromagnetism decl_use
alkali_halogen_ionic in IndisputableMonolith.Chemistry.IonicBond decl_use
madelung_nacl_pos in IndisputableMonolith.Chemistry.IonicBond decl_use
londonDispersionProxy in IndisputableMonolith.Chemistry.VanDerWaals decl_use
buildPeelingResult in IndisputableMonolith.Complexity.SAT.PC decl_use
extractFromPC in IndisputableMonolith.Complexity.SAT.PC decl_use
InputSet in IndisputableMonolith.Complexity.SAT.PC decl_use
PC in IndisputableMonolith.Complexity.SAT.PC decl_use
PeelingResult in IndisputableMonolith.Complexity.SAT.PC decl_use
cone_bound_export in IndisputableMonolith.ConeExport.Theorem decl_use
ConeEntropyFacts in IndisputableMonolith.ConeExport.Theorem decl_use
display_null_condition in IndisputableMonolith.Constants.KDisplay decl_use
display_rate_matches_structural_rate in IndisputableMonolith.Constants.KDisplay decl_use
display_ratio_scale_invariant in IndisputableMonolith.Constants.KDisplay decl_use
display_speed_eq_c in IndisputableMonolith.Constants.KDisplay decl_use
display_speed_eq_c_of_nonzero in IndisputableMonolith.Constants.KDisplay decl_use
display_speed_positive in IndisputableMonolith.Constants.KDisplay decl_use
ell0_div_tau0_eq_c in IndisputableMonolith.Constants.KDisplay decl_use
K_gate_check in IndisputableMonolith.Constants.KDisplay decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

U in IndisputableMonolith.Constants.RSNativeUnits decl_use