theorem
proved
compositeFailureMode_count
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Materials.CompositeFailureModesFromConfigDim on GitHub at line 26.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
23 | interfacialDebonding
24 deriving DecidableEq, Repr, BEq, Fintype
25
26theorem compositeFailureMode_count : Fintype.card CompositeFailureMode = 5 := by decide
27
28structure CompositeFailureModesCert where
29 five_modes : Fintype.card CompositeFailureMode = 5
30
31def compositeFailureModesCert : CompositeFailureModesCert where
32 five_modes := compositeFailureMode_count
33
34end IndisputableMonolith.Materials.CompositeFailureModesFromConfigDim