Mathlib v3 is deprecated. Go to Mathlib v4

Theorem 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 algebra_map_injective View on Github →