Commit 2020-02-28 15:33 07608293

feat(ring_theory): Fractional ideals (#2062)

• Some WIP work on fractional ideals
• Fill in the sorry
• A lot of instances for fractional_ideal
• Show that an invertible fractional ideal I has inverse 1 : I
• Cleanup and documentation
• Move has_div submodule to algebra_operations
• More cleanup and documentation
• Explain the non_zero_divisors R in the quotient section
• whitespace Co-Authored-By: Scott Morrison scott@tqft.net
• has_inv instance for fractional_ideal
• set.univ.image -> set.range
• Fix: mem_div_iff.mpr should be mem_div_iff.mp (but both reduce to reflexivity anyway)
• Add mem_div_iff_smul_subset Since that is how the definition of I / J is traditionally done, but it is not as convenient to work with, I didn't change the definition but added a lemma stating the two are equivalent
• whitespace again (it got broken because I merged changes incorrectly)
• Fix unused argument to inv_nonzero