[Merged by Bors] - feat: Define intNorm and intTrace.

[erdOne]

---

[erdOne]

The connection to RingOfIntegers.norm will be provided in a later PR.

[jcommelin]

Is "AKLB setup" standard terminology (in mathlib)?
It's the first time I see it.

[erdOne]

In this file, we assume `A` is an integrally closed domain; `K` is the fraction ring of `A`;
`L` is a finite (separable) extension of `K`; `B` is the integral closure of `A` in `L`.
We call this the AKLB setup.

is in the module docstring.

[jcommelin]

I see. That makes sense. But I'm not sure that we should assume this kind of info in docstrings, since they show up outside the context of the file.
Maybe add

Suggested change

	/-- The restriction of the trace on `L/K` restricted onto `B/A` in an AKLB setup.
	/-- The restriction of the trace on `L/K` restricted onto `B/A` in an AKLB setup (see module docstring).

for now...

[erdOne]

I think this terminology also appears in some literature, for example Ash's A Course In Algebraic Number Theory.
Maybe I can expand the docstring into a library note in a future PR and reference it here.
Have we implemented library note in lean4 yet?

[erdOne]

I kept the docstring as is for now. This is an auxiliary definition that probably won't be used outside this file.

[xroblot]

LGTM. How do the results in this PR relate to what Riccardo did in NumberTheory.NumberField.Norm?

[erdOne]

The connection needs some other stuff (for example #9444) and will come in a later PR.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style

[riccardobrasca]

I somehow missed this PR, sorry. Anyway the new intNorm could completely replace RingOfIntegers.norm, right?

[erdOne]

Maybe yes. This might not work when k and K aren't number fields but we might not care.
I'd still keep RingOfIntegers.norm but redefine it in terms of intNorm though.