# 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.