mathlib
da420a8c - refactor(*): reduce dependencies on ring_theory.ideal.quotient_operations (#18530)

Commit

2 years ago

refactor(*): reduce dependencies on ring_theory.ideal.quotient_operations (#18530) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

jcommelin

Parents