OAI/Combinatorics/BalancedRyser/Incidence/StabilityCoprimeReduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.StabilityCoprimeReduction.exists_coprime_grid_reduction line 14
2. theorem OAI.Balanced.StabilityCoprimeReduction.redeiLeadingProduct_monic line 48
3. theorem OAI.Balanced.StabilityCoprimeReduction.redeiLeadingProduct_natDegree line 53
4. theorem OAI.Balanced.StabilityCoprimeReduction.multiplier_ne_zero_of_low_remainder line 60
5. theorem OAI.Balanced.StabilityCoprimeReduction.card_le_card_add_auxiliary_bound line 72
6. theorem OAI.Balanced.StabilityCoprimeReduction.exists_coprime_redei_identity line 79