recognition /
Physics /
Physics.QuantumHallEffect /
explainer
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)
35 structure ChernNumber where
36 value : ℤ
37 -- Chern number is integer-valued by definition (topological quantization)
38
39 /-- The Hall conductance in units of e²/h equals the Chern number. -/
depends on (11)
Lean names referenced from this declaration's body.
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
quantization
in IndisputableMonolith.LedgerUnits
decl_use
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
value
in IndisputableMonolith.QFT.SpinStatistics
decl_use