Commit 2022-11-22 12:28 31c458dc

View on Github →

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.

Estimated changes