Commit 2020-06-08 13:54 a7930425

feat(ring_theory/fractional_ideal): pushforward of fractional ideals (#2984) Extend submodule.map to fractional ideals by showing that the pushforward is also fractional. For this, we need a slightly tweaked definition of fractional ideal: if we localize R at the submonoid S, the old definition required a nonzero x : R such that xI ≤ R, and the new definition requires x ∈ S instead. In the most common case, S = non_zero_divisors R, the results are exactly the same, and all operations are still the same. A practical use of these pushforwards is included: canonical_equiv states fractional ideals don't depend on choice of localization map.