OAI/Algebra/Determinantal/BranchConductor.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.ReducedBranchConductor.gradientIdeal line 9
  2. def OAI.PermanentBorder.ReducedBranchConductor.enlargedGradientIdeal line 11
  3. lemma OAI.PermanentBorder.ReducedBranchConductor.map_enlarged_le line 15
  4. lemma OAI.PermanentBorder.ReducedBranchConductor.root_generates line 55
  5. lemma OAI.PermanentBorder.ReducedBranchConductor.root_separable line 61
  6. theorem OAI.PermanentBorder.ReducedBranchConductor.irreducible_realization line 80
  7. lemma OAI.PermanentBorder.FactorNormalization.lift_monic_factor line 164
  8. theorem OAI.PermanentBorder.FactorNormalization.exists_factors line 174
  9. def OAI.PermanentBorder.FactorNormalization.cofactor line 201
  10. lemma OAI.PermanentBorder.FactorNormalization.factor_mul_cofactor line 204
  11. lemma OAI.PermanentBorder.FactorNormalization.cofactor_dvd_of_ne line 209
  12. def OAI.PermanentBorder.FactorNormalization.component line 227
  13. lemma OAI.PermanentBorder.FactorNormalization.component_mk line 233
  14. lemma OAI.PermanentBorder.FactorNormalization.components_injective line 240
  15. theorem OAI.PermanentBorder.FactorNormalization.reconstruct line 259
  16. theorem OAI.PermanentBorder.ReducedBranchConductor.reduced_local_realization line 289
  17. lemma OAI.PermanentBorder.ReducedBranchConductor.gradient_map line 327
  18. lemma OAI.PermanentBorder.ReducedBranchConductor.enlarged_map_le line 333
  19. lemma OAI.PermanentBorder.ReducedBranchConductor.map_tower line 348
  20. def OAI.PermanentBorder.ReducedBranchConductor.genericChange line 353
  21. lemma OAI.PermanentBorder.ReducedBranchConductor.genericChange_mk line 359
  22. lemma OAI.PermanentBorder.ReducedBranchConductor.polynomial_lattice_local_global line 377
  23. lemma OAI.PermanentBorder.ReducedBranchConductor.polynomial_residue_algClosed line 418
  24. theorem OAI.PermanentBorder.ReducedBranchConductor.reduced_global_realization line 431