def
definition
catalystSelectivityCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Chemistry.CatalystSelectivityFromJCost on GitHub at line 33.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
30structure CatalystSelectivityCert where
31 five_regimes : Fintype.card SelectivityRegime = 5
32
33def catalystSelectivityCert : CatalystSelectivityCert where
34 five_regimes := selectivityRegime_count
35
36end IndisputableMonolith.Chemistry.CatalystSelectivityFromJCost