feat(ring_theory/ideal): ideal norm evaluation lemmas (#17299)
This PR continues on #17203 by adding a couple lemmas on the ideal norm of some specific ideals:
* the norm of `⊥` and `⊤`
* the norm of an ideal `I : ideal S` given an additive isomorphism between `I` and `S`
* the norm of the ideal generated by `a`
* the norm of the ideal generated by `insert a s`
It also adds a selection of dependent lemmas. I couldn't find a really neat place for some of them: I think the current places are the least worst but I am very much open to suggestions.
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
