Commit 2023-11-19 10:31 6f853a60

View on Github →

feat: move the lemma Algebra.coe_norm_int (#8481) The following lemma:

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

is currently in NumberField.Units but it belongs to NumberField.Norm

Estimated changes

added theorem Algebra.coe_norm_int
deleted theorem Algebra.coe_norm_int