Commit 2023-06-21 01:06 721f3903

View on Github →

feat: port NumberTheory.NumberField.Basic (#5309)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/NumberField/Basic.lean

added theorem Int.not_isField

added theorem NumberField.RingOfIntegers.isIntegral_coe

added theorem NumberField.RingOfIntegers.map_mem

added theorem NumberField.RingOfIntegers.not_isField

added theorem NumberField.RingOfIntegers.rank

added theorem NumberField.integralBasis_apply

added theorem NumberField.isIntegral_of_mem_ringOfIntegers

added theorem NumberField.mem_ringOfIntegers

added def NumberField.ringOfIntegers

added def NumberField.ringOfIntegersAlgebra