Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.not_is_field

Modification history

2022-10-03 14:28
src/number_theory/number_field/basic.lean
refactor(number_theory): reorganize number field results into new subfolder (#16764) …
Modified int.not_is_fieldView on Github →
2022-04-06 12:59
src/number_theory/number_field.lean
feat(algebra/parity): introduce `is_square` and, via `to_additive`, also `even` (#13037) …
Modified int.not_is_fieldView on Github →
2022-03-07 21:31
src/number_theory/number_field.lean
chore(number_theory/number_field): golf `int.not_is_field` (#12451) …
Modified int.not_is_fieldView on Github →
2022-02-11 15:45
src/number_theory/number_field.lean
feat(number_theory/number_field/basic) : the ring of integers of a number field is not a field (#11956)
Added int.not_is_fieldView on Github →