OAI/NumberTheory/Ostmann/Characters/TemplateDiagonalMatching.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Characters.TemplateDiagonalMatching.prime_tuple_equal_product_matchline 15 - theorem
OAI.Ostmann.Characters.TemplateDiagonalMatching.existsUnique_prime_tuple_matchingline 26 - theorem
OAI.Ostmann.Characters.TemplateDiagonalMatching.tuple_prior_mass_eqline 45 - theorem
OAI.Ostmann.Characters.TemplateDiagonalMatching.matched_tuple_prior_mass_eqline 63