Commit 2022-11-22 12:28 31c458dc

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.