Commit 2022-02-18 18:09 018c7289
View on Github →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.