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`
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
