OAI/Algebra/Determinantal/Monogenic.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PermanentBorder.NormalizationMonogenic.adjoin_eq_top_of_nilpotent_reduction line 11
  2. lemma OAI.PermanentBorder.NormalizationMonogenic.adjoin_uniformizer_eq_top line 38
  3. lemma OAI.PermanentBorder.NormalizationMonogenic.nilradical_eq_span_of_mod_square line 71
  4. lemma OAI.PermanentBorder.NormalizationMonogenic.exists_adjoin_eq_top line 98
  5. lemma OAI.PermanentBorder.NormalizationMonogenic.adjoin_eq_top_of_residue_surjective line 191
  6. lemma OAI.PermanentBorder.NormalizationMonogenic.exists_adjoin_eq_top_of_residue_principal line 212
  7. lemma OAI.PermanentBorder.NormalizationMonogenic.exists_adjoin_eq_top_of_principal line 236
  8. def OAI.PermanentBorder.NormalizationDerivation.extendEtale line 253
  9. lemma OAI.PermanentBorder.NormalizationDerivation.extendEtale_algebraMap line 259
  10. def OAI.PermanentBorder.NormalizationDerivation.coeffDeriv line 272
  11. lemma OAI.PermanentBorder.NormalizationDerivation.coeffDeriv_coeff line 275
  12. lemma OAI.PermanentBorder.NormalizationDerivation.coeffDeriv_C line 278
  13. lemma OAI.PermanentBorder.NormalizationDerivation.coeffDeriv_X line 284
  14. def OAI.PermanentBorder.NormalizationDerivation.hamiltonian line 290
  15. lemma OAI.PermanentBorder.NormalizationDerivation.hamiltonian_self line 294
  16. lemma OAI.PermanentBorder.NormalizationDerivation.hamiltonian_C line 299
  17. lemma OAI.PermanentBorder.NormalizationDerivation.hamiltonian_X line 303
  18. lemma OAI.PermanentBorder.NormalizationDerivation.hamiltonian_preserves_equation line 307
  19. def OAI.PermanentBorder.NormalizationDerivation.scaledExtension line 320
  20. lemma OAI.PermanentBorder.NormalizationDerivation.scaledExtension_aeval line 330
  21. lemma OAI.PermanentBorder.NormalizationDerivation.scaledExtension_algebraMap line 338
  22. lemma OAI.PermanentBorder.NormalizationDerivation.scaledExtension_generator line 345
  23. lemma OAI.PermanentBorder.NormalizationDerivation.adjoin_fraction_generator line 363
  24. lemma OAI.PermanentBorder.NormalizationDerivation.exists_scaled_normalization_derivation line 405