Commit 2023-06-21 21:04 e032d377

View on Github →

feat: port NumberTheory.NumberField.Norm (#5353)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Created Mathlib/NumberTheory/NumberField/Norm.lean

added theorem RingOfIntegers.coe_algebraMap_norm

added theorem RingOfIntegers.coe_norm_algebraMap

added theorem RingOfIntegers.dvd_norm

added theorem RingOfIntegers.isUnit_norm

added theorem RingOfIntegers.isUnit_norm_of_isGalois

added theorem RingOfIntegers.norm_algebraMap

added theorem RingOfIntegers.norm_norm