Algebra.norm ℤ

Stream: Is there code for X?

[Andrew Yang]

Do we have this somewhere? Is there an easy proof to it?

import Mathlib.NumberTheory.NumberField.Norm

open scoped NumberField

example {K : Type*} [Field K] [NumberField K] (x : 𝓞 K) :
  Algebra.norm ℤ x = Algebra.norm ℚ (x : K) := sorry

[Riccardo Brasca]

Not sure it is literally this, but docs#RingOfIntegers.norm_apply_coe should be very close.

[Riccardo Brasca]

In any case docs#RingOfIntegers.norm is there exactly to consider the norm of an element of the ring of integers

[Andrew Yang]

RingOfIntegers.normis defined by restricting Algebra.norm K onto 𝓞 K, but I don't think we know that it is equal to Algebra.norm (𝓞 K).

[Xavier Roblot]

I think what you want is docs#Algebra.norm_localization

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

Ah yes, sorry. I am always a little bit worried about Algebra.norm K, since in the relative case it is not the right notion.

[Andrew Yang]

Xavier Roblot said:

I think what you want is docs#Algebra.norm_localization

Thanks! Works like a charm.