OAI/NumberTheory/Ostmann/Characters/SparseScalarNorm.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The scalar block stays positive while retaining its decrease
- theorem
OAI.Ostmann.sparse_scalar_norm_boundsline 10