Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-11 15:45 edefc116

View on Github →

feat(number_theory/number_field/basic) : the ring of integers of a number field is not a field (#11956)

Estimated changes

Modified src/data/int/char_zero.lean

added theorem ring_hom.injective_int

Modified src/number_theory/number_field.lean

added theorem int.not_is_field

added theorem number_field.ring_of_integers.not_is_field