Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-10 08:56 49bb92dc

View on Github →

feat(ring_theory/dedekind_domain): definitions (#4000) Defines is_dedekind_domain in three variants:

  1. is_dedekind_domain: Noetherian, Integrally closed, Krull dimension 1, thanks to @Vierkantor
  2. is_dedekind_domain_dvr: Noetherian, localization at every nonzero prime is a DVR
  3. is_dedekind_domain_inv: Every nonzero ideal is invertible. TODO: prove that these definitions are equivalent. This PR also includes some misc. lemmas required to show the definitions are independent of choice of fraction field. Co-Authored-By: mushokunosora knaka3435@gmail.com Co-Authored-By: faenuccio filippo.nuccio@univ-st-etienne.fr Co-Authored-By: Vierkantor vierkantor@vierkantor.com

Estimated changes

modified theorem alg_equiv.bijective
modified theorem alg_equiv.coe_alg_hom
modified theorem alg_equiv.coe_ring_equiv
modified theorem alg_equiv.commutes
modified theorem alg_equiv.injective
modified theorem alg_equiv.map_add
modified theorem alg_equiv.map_mul
modified theorem alg_equiv.map_one
modified theorem alg_equiv.map_sum
modified theorem alg_equiv.map_zero
modified theorem alg_equiv.surjective
added theorem subalgebra.mem_map
added theorem submodule.map_div
added structure is_dedekind_domain_dvr
added theorem is_dedekind_domain_iff
added structure is_dedekind_domain_inv
added theorem ideal.span_mul_span'
added def fraction_ring.of
deleted def of