Mathlib v3 is deprecated. Go to Mathlib v4

Def function_field.ring_of_integers

Modification history

2022-02-08 12:43
src/number_theory/function_field.lean
feat(*): localized `R[X]` notation for `polynomial R` (#11895) …
Modified function_field.ring_of_integersView on Github →
2021-09-02 15:21
src/number_theory/function_field.lean
feat(number_theory): define number fields, function fields and their rings of integers (#8701) …
Added function_field.ring_of_integersView on Github →