OAI/NumberTheory/PiExponent/Jets/JetProductLocalization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.JetProductLocalization.residueAlgHom line 13
2. theorem OAI.PiExponent.JetProductLocalization.residue_ne_zero_iff_isUnit line 17
3. theorem OAI.PiExponent.JetProductLocalization.residue_polynomial_aeval line 24
4. theorem OAI.PiExponent.JetProductLocalization.residue_truncatedCoordinates_succ line 30
5. theorem OAI.PiExponent.JetProductLocalization.logarithmicIdeal_eq_top_of_residue_ne line 42
6. theorem OAI.PiExponent.JetProductLocalization.map_powerIdeal_eq_top_of_ne line 67
7. theorem OAI.PiExponent.JetProductLocalization.map_polynomialIdeal line 85
8. theorem OAI.PiExponent.JetProductLocalization.map_polynomialIdeal_eq_selected line 98
9. theorem OAI.PiExponent.JetProductLocalization.map_polynomialIdeal_eq_top_outside line 114