Mathlib v3 is deprecated. Go to Mathlib v4

Theorem field.localization_map_bijective

Modification history

2022-03-02 10:22

src/ring_theory/localization/basic.lean

chore(ring_theory/localization): `localization_map_bijective` rename & `field` instance version (#12375)

Added field.localization_map_bijective View on Github →