Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 19:34 aea21af1

View on Github →

feat(ring_theory): is_dedekind_domain_inv implies is_dedekind_domain (#8315) Co-Authored-By: Ashvni ashvni.n@gmail.com Co-Authored-By: Filippo A. E. Nuccio filippo.nuccio@univ-st-etienne.fr

Estimated changes

Modified src/ring_theory/dedekind_domain.lean

added theorem fractional_ideal.adjoin_integral_eq_one_of_is_unit

added theorem is_dedekind_domain_inv.dimension_le_one

added theorem is_dedekind_domain_inv.integrally_closed

added theorem is_dedekind_domain_inv.inv_mul_eq_one

added theorem is_dedekind_domain_inv.is_dedekind_domain

added theorem is_dedekind_domain_inv.is_noetherian_ring

added theorem is_dedekind_domain_inv.mul_inv_eq_one

modified theorem is_dedekind_domain_inv_iff

added theorem mul_inv_cancel_iff_is_unit

Modified src/ring_theory/fractional_ideal.lean

modified theorem fractional_ideal.mem_coe

added theorem fractional_ideal.mem_coe_ideal_of_mem

Modified src/ring_theory/principal_ideal_domain.lean

added theorem is_field.is_principal_ideal_ring