Commit 2023-08-02 23:22 c87bb109

View on Github →

chore: make ringOfIntegersAlgebra an instance (#6244)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Basic.lean

deleted def NumberField.ringOfIntegersAlgebra

Modified Mathlib/NumberTheory/NumberField/Norm.lean

Modified Mathlib/NumberTheory/NumberField/Units.lean