Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-16 21:24 c64b67ed

View on Github →

feat(ring_theory/localization): revamp, ideal embedding (#481)

Estimated changes

Modified src/ring_theory/localization.lean

modified def localization.at_prime

added def localization.away.inv_self

modified def localization.away

added theorem localization.coe_add

added theorem localization.coe_mul

added theorem localization.coe_mul_of

added theorem localization.coe_neg

added theorem localization.coe_one

added theorem localization.coe_pow

added theorem localization.coe_sub

added theorem localization.coe_zero

added def localization.fraction_ring

modified def localization.inv_aux

added def localization.le_order_embedding

added theorem localization.map_comap

added def localization.of

added theorem localization.of_add

deleted def localization.of_comm_ring

added theorem localization.of_eq_div

added theorem localization.of_eq_mul_of_one

added theorem localization.of_mul

added theorem localization.of_mul_cancel_left

added theorem localization.of_mul_cancel_right

added theorem localization.of_mul_of

added theorem localization.of_neg

added theorem localization.of_one

added theorem localization.of_pow

added theorem localization.of_self''

added theorem localization.of_self'

added theorem localization.of_self

added theorem localization.of_sub

added theorem localization.of_zero

deleted def localization.quotient_ring.field.of_integral_domain

deleted def localization.quotient_ring

modified def localization.r

modified theorem localization.r_of_eq

modified theorem localization.symm