ring_division): remove `open_locale classical` (#19182)

Commit

2 years ago

refactor(data/polynomial/ring_division): remove `open_locale classical` (#19182) This makes the lemmas strictly more general.

Author

eric-wieser

Parents