Theorem RingOfIntegers.isUnit_norm_of_isGalois

Modification history

2025-10-12 17:44
Mathlib/NumberTheory/NumberField/Norm.lean
feat: remove separability assumption from Algebra.norm_eq_norm_adjoin and Algebra.norm_eq_prod_roots (#30448) …
Modified RingOfIntegers.isUnit_norm_of_isGaloisView on Github →
2023-06-21 21:04
Mathlib/NumberTheory/NumberField/Norm.lean
feat: port NumberTheory.NumberField.Norm (#5353)
Added RingOfIntegers.isUnit_norm_of_isGaloisView on Github →