OAI/NumberTheory/PiExponent/LocalAlgebra/RegularDegreePositivity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSiegel.W20.regular_sequence_ideal_ne_top line 15
2. theorem OAI.PiExponentSiegel.W20.regular_sequence_term_not_isUnit line 23
3. theorem OAI.PiExponentSiegel.W20.regular_sequence_term_ne_zero line 31
4. theorem OAI.PiExponentSiegel.W20.regular_homogeneous_degrees_pos line 51
5. theorem OAI.PiExponentSiegel.W20.regular_homogeneous_degree_product_ne_zero line 72