OAI/NumberTheory/PiExponent/LocalAlgebra/WeightedBezoutBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.WeightedBezout.pointLength line 12
2. theorem OAI.PiExponent.WeightedBezout.pointLength_translatedPowerSubstitution line 18
3. theorem OAI.PiExponent.WeightedBezout.finite_length_of_rank_bound line 25
4. theorem OAI.PiExponent.WeightedBezout.weighted_bound_of_scaled_natural line 38
5. theorem OAI.PiExponent.WeightedBezout.weight_product_comparison line 61
6. theorem OAI.PiExponent.WeightedBezout.pointLength_mul_le_of_substituted_degree line 77
7. theorem OAI.PiExponent.WeightedBezout.pointLength_mul_le line 100
8. theorem OAI.PiExponent.WeightedBezout.rational_pointLength_bound line 111