OAI/NumberTheory/TwoPoint/Bounds/WeightedTupleDesignation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual designated tuple-word majorant has precisely the weight used by column rank.

  1. theorem OAI.TwoPointCorrelations.weighted_designation_le_tuple_weight line 13