def
definition
nanoScienceCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.NanoScienceFromRS on GitHub at line 39.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
36 five_phenomena : Fintype.card NanoscalePhenomenon = 5
37 five_structures : Fintype.card NanostructureType = 5
38
39def nanoScienceCert : NanoScienceCert where
40 five_phenomena := nanoscalePhenomenonCount
41 five_structures := nanostructureTypeCount
42
43end IndisputableMonolith.Physics.NanoScienceFromRS