OAI/NumberTheory/PiExponent/LocalAlgebra/RegularParameterSelection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSiegel.W58.polynomialLocal_regular_prefix_maximal_not_associated line 16
2. theorem OAI.PiExponentSiegel.W58.polynomialLocal_exists_constant_regular_parameters line 37
3. theorem OAI.PiExponentSiegel.W58.polynomialLocal_exists_constant_regular_parameters_actual_height line 58
4. theorem OAI.PiExponentSiegel.W58.polynomialLocal_exists_degree_bounded_regular_parameters line 74