Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function_field.ring_of_integers.not_is_field

Modification history

2022-03-17 11:06

src/number_theory/function_field.lean

feat(number_theory/function_field): the ring of integers of a function field is not a field (#12705)

Added function_field.ring_of_integers.not_is_field View on Github →