Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-17 11:06 b1bf390d

View on Github →

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

Estimated changes

Modified src/data/polynomial/div.lean

added theorem polynomial.not_is_field

Modified src/number_theory/function_field.lean

added theorem algebra_map_injective

added theorem function_field.ring_of_integers.algebra_map_injective

added theorem function_field.ring_of_integers.not_is_field