Commit 2021-07-29 15:02 a4f16538

View on Github →

feat(ring_theory): Dedekind domains have invertible fractional ideals (#8396) This PR proves the other side of the equivalence is_dedekind_domain → is_dedekind_domain_inv, and uses this to provide a comm_group_with_zero (fractional_ideal A⁰ K) instance. 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 coe_ideal_le_self_mul_inv

added theorem exists_multiset_prod_cons_le_and_prod_not_le

added theorem fractional_ideal.coe_ideal_mul_inv

added theorem fractional_ideal.exists_not_mem_one_of_ne_bot

added theorem fractional_ideal.mul_inv_cancel

added theorem fractional_ideal.mul_inv_cancel_of_le_one

added theorem fractional_ideal.one_inv

added theorem fractional_ideal.one_mem_inv_coe_ideal

added theorem inv_anti_mono

added theorem is_dedekind_domain_iff_is_dedekind_domain_inv

added theorem le_self_mul_inv

added theorem mem_inv_iff

Modified src/ring_theory/fractional_ideal.lean

added theorem fractional_ideal.eq_zero_or_one

added theorem fractional_ideal.eq_zero_or_one_of_is_field