OAI/NumberTheory/PiExponent/LocalAlgebra/TriangularLocalParameters.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.scalar_top_eq_principal line 22
  2. def OAI.PiExponentSiegel.W10.TriangularLocalParameters.principalModuleQuotientEquiv line 26
  3. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.principalModuleQuotientEquiv_mk line 31
  4. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.regular_cons_of_principal_kernel line 39
  5. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.ofList_cons_eq_comap line 59
  6. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.lift_parameters line 66
  7. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.regular_element_of_ne_zero line 82
  8. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.singleton_parameter_regular line 85
  9. def OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstPolynomial line 99
  10. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstPolynomial_ne_zero line 101
  11. def OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstLocalParameter line 106
  12. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstLocalParameter_ne_zero line 109
  13. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstLocalParameter_span line 113
  14. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.oneVariable_parameters line 127
  15. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.zeroVariable_maximal_eq_bot line 142
  16. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.zeroVariable_parameters line 153
  17. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.maximal_coefficient_contraction line 169
  18. def OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstCoordinateContraction line 177
  19. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstCoordinateContraction_isMaximal line 180
  20. def OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstCoordinatePolynomial line 195
  21. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstCoordinatePolynomial_irreducible line 198
  22. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstCoordinatePolynomial_mem line 206
  23. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstCoordinateIdeal_le line 211
  24. theorem OAI.PiExponentSiegel.W10.TriangularLocalParameters.firstCoordinateRelation_ne_zero line 216