mathlib3

018c7289 - refactor(ring_theory/fractional_ideal): rename lemmas for dot notation, add coe_pow (#12080)

refactor(ring_theory/fractional_ideal): rename lemmas for dot notation, add coe_pow (#12080) This replaces `fractional_ideal.fractional_mul` with `is_fractional.mul` and likewise for the other operations. The bundling was a distraction for the content of the lemmas anyway.