OAI/NumberTheory/Ostmann/Characters/CharacterBandSelection.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The lower shell, bulk band and rich upper block are selected together
- theorem
OAI.Ostmann.exists_character_band_selectionline 12