operations): add algebra structure on quotient (#5703)

Commit

4 years ago

feat(ring_theory/ideal/operations): add algebra structure on quotient (#5703) I added very basic stuff about `R/I` as an `R`-algebra that are missing in mathlib.

Author

riccardobrasca

Parents

f3d3d046

mathlib3 db617b3c - feat(ring_theory/ideal/operations): add algebra structure on quotient (#5703)

mathlib3
db617b3c - feat(ring_theory/ideal/operations): add algebra structure on quotient (#5703)