def
definition
countLegal
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Crystallography.SelectionRules on GitHub at line 35.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
32 (Finset.range 8).sum (fun i => w (i0 + i))
33
34/‑ Count legal triads in a finite list. -/
35def countLegal (ts : List Triad) : ℕ :=
36 ts.countP (fun t => legalTriad t)
37
38end SelectionRules
39end Crystallography
40end IndisputableMonolith