def
definition
magneticReconnectionCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Astrophysics.MagneticReconnectionFromJCost on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
31 five_regimes : Fintype.card ReconnectionRegime = 5
32 trigger_threshold : CanonicalCert
33
34noncomputable def magneticReconnectionCert : MagneticReconnectionCert where
35 five_regimes := reconnectionRegimeCount
36 trigger_threshold := cert
37
38end IndisputableMonolith.Astrophysics.MagneticReconnectionFromJCost