operation): add some extra definitions in the `double_quot` section (#9649)

Commit

4 years ago

feat(ring_theory/ideal/operation): add some extra definitions in the `double_quot` section (#9649)

Author

Paul-Lez

Parents