Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function_field.ring_of_integers.algebra_map_injective

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.algebra_map_injectiveView on Github →