Commit 2024-01-17 13:26 7f5d26d3

feat: Generalize absNorm to fractional ideals (#9613) This PR defines the absolute ideal norm of a fractional ideal I : FractionalIdeal R⁰ K where K is a fraction field of R as a zero-preserving group homomorphism with values in ℚ and proves that it generalises the norm on (integral) ideals (and some other classical result). Also in this PR:

• Add the directory Mathlib/RingTheory/FractionalIdeal and move the file Mathlib/RingTheory/FractionalIdeal.lean to Mathlib/RingTheory/FractionalIdeal/Basic.lean. The new results are in Mathlib/RingTheory/FractionalIdeal/Norm.lean
• Define the numerator and denominator of a fractional ideal. These are used to define the norm. Also define a linear equiv between a fractional ideal and its numerator.
• Several technical lemmas.