OAI/RingTheory/Multiplicity/LechLengthLe.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.length_le_add_of_exact line 20
2. lemma OAI.Lech.ParameterBound.length_mul_le line 41
3. lemma OAI.Lech.ParameterBound.length_pow_le line 97
4. lemma OAI.Lech.ParameterBound.length_parameter_powers_le line 107
5. lemma OAI.Lech.length_quotient_le line 137
6. lemma OAI.Lech.colength_polynomial_bound line 145
7. def OAI.Lech.FrobeniusGrowth.powerIdeal line 203
8. lemma OAI.Lech.FrobeniusGrowth.pow_mem_powerIdeal line 206
9. lemma OAI.Lech.FrobeniusGrowth.powerIdeal_eq_map line 209
10. lemma OAI.Lech.FrobeniusGrowth.pigeonhole line 214
11. lemma OAI.Lech.FrobeniusGrowth.linear_power_containment line 235
12. lemma OAI.Lech.FrobeniusGrowth.quotient_power_length line 252
13. lemma OAI.Lech.FrobeniusGrowth.quotient_dimension_lt line 265
14. lemma OAI.Lech.FrobeniusGrowth.quotient_colength_bound line 273
15. theorem OAI.Lech.FrobeniusGrowth.normalized_error_bound line 311
16. theorem OAI.Lech.FrobeniusGrowth.normalized_error_tendsto line 344
17. lemma OAI.Lech.FrobeniusGrowth.normalized_error_tendstoENNReal line 363
18. lemma OAI.Lech.FrobeniusGrowth.frobenius_error_tendstoENNReal line 381
19. lemma OAI.Lech.RootTower.perfectClosure_flat line 401
20. theorem OAI.Lech.PerfectDomainStages.frobenius_colength_tendsto line 438