OAI/Combinatorics/Progressions/Polynomial/BoundedRootDegreeEquivalence.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.NativeMultidegreeNilcharacter.exists_dilation_degree_equivalenceline 12 - theorem
OAI.Erdos3.NativeMultidegreeNilcharacter.exists_root_degree_equivalenceline 46 - theorem
OAI.Erdos3.NativeMultidegreeNilcharacter.exists_uniform_dilation_degree_equivalenceline 113 - theorem
OAI.Erdos3.NativeMultidegreeNilcharacter.exists_uniform_root_degree_equivalenceline 151 - theorem
OAI.Erdos3.NativeMultidegreeNilcharacter.exists_bounded_root_degree_equivalenceline 214