Junyan Xu

@riccardobrasca Thanks for that :) I was distracted and will need a few more days before I get back to this.

I'm finally back working on this PR; sorry for the long delay! In addition to the request to add `ideal.quotient.alg_hom_ext`, I also plan to prove `localization.away` is finitely presented ([algebra.finite_presentation](https://leanprover-community.github.io/mathlib_docs/ring_theory/finiteness.html#algebra.finite_presentation)),...

@nick-kuhn So you didn't use adjoin_root API? Notice that `adjoin_root f = (polynomial R ⧸ ideal.span {f})` definitionally, and it would be nice to show finite presentation more generally for...

Alright, the proof of ``` lemma is_localization.away.finite_presentation {R} [comm_ring R] (r : R) {S} [comm_ring S] [algebra R S] [is_localization.away r S] : algebra.finite_presentation R S := ``` is now...

Maybe we should define a degree for every map (ideally homomorphism) from the `add_monoid` to an arbitrary `linear_ordered_monoid`. This would unify multiple notions: for polynomials and Laurent polynomials, the `linear_ordered_monoid`...

@adomani I only just subscribed to this PR so I am not aware of the prior discussions; can you point to the relevant ones? I wonder why you didn't prove...

> The "total degree" operation is spelt x.sup (λ x, x.1 + x.2), which still works with the lemma in this PR I think. Oh indeed, thanks for pointing that...

> However, non-linearly ordered target monoids do show up in maths as well. You can search for multigraded {rings, ideals, Hilbert series,...} to see some of these. In these situations,...

> But would the proofs so far have gotten easier with a stronger assumption? The proofs may not get easier, but the statements will certainly be shorter with `[linear_ordered_add_comm_monoid B]`...

I'm not against generality; in fact, I just found one use case in mathlib where `B` is not a linear_order: [mv_polynomial.degrees](https://leanprover-community.github.io/mathlib_docs/data/mv_polynomial/variables.html#mv_polynomial.degrees), so I'm in favor of keeping the smilattice_inf versions...