Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-09 17:00 f098c16e

View on Github →

feat(ring_theory/localization): more lemmas and defs about fields of fractions (#3005)

Estimated changes

Modified src/ring_theory/localization.lean

modified theorem eq_zero_of_ne_zero_of_mul_eq_zero

added theorem fraction_map.is_unit_map_of_injective

added theorem fraction_map.lift_mk'

added theorem fraction_map.mk'_eq_div

added theorem fraction_ring.mk_eq_div

added def fraction_ring

added theorem map_mem_non_zero_divisors

added theorem map_ne_zero_of_mem_non_zero_divisors

modified theorem mem_non_zero_divisors_iff_ne_zero

added def of