mathlib3
76ba1b64 - chore(ring_theory/finiteness): make `finite_presentation.{quotient,mv_polynomial}` protected (#10091)

Commit

4 years ago

chore(ring_theory/finiteness): make `finite_presentation.{quotient,mv_polynomial}` protected (#10091) This lets us clean up some `_root_`s This also golfs a proof

Author

eric-wieser

Parents

8658f40c

mathlib3 76ba1b64 - chore(ring_theory/finiteness): make `finite_presentation.{quotient,mv_polynomial}` protected (#10091)

mathlib3
76ba1b64 - chore(ring_theory/finiteness): make `finite_presentation.{quotient,mv_polynomial}` protected (#10091)