Commit 2023-06-22 05:54 81c3108d

View on Github →

feat: port NumberTheory.NumberField.Units (#5359)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/NumberField/Units.lean

added theorem Rat.RingOfIntegers.isUnit_iff

added theorem isUnit_iff_norm