Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-08 11:25 c852939f

View on Github →

feat(ring_theory): move localization

Estimated changes

Modified algebra/group.lean

Modified algebra/group_power.lean

added def powers

Deleted algebra/localization.lean

deleted def loc.add

deleted def loc.add_aux

deleted def loc.loc

deleted def loc.mul

deleted def loc.mul_aux

deleted def loc.neg

deleted def loc.neg_aux

Modified algebra/module.lean

added theorem is_submodule.eq_univ_of_contains_unit

added theorem is_submodule.univ_of_one_mem

Modified algebra/ring.lean

added theorem is_ring_hom.map_neg

added theorem is_ring_hom.map_sub

added theorem is_ring_hom.map_zero

added def nonunits

Modified data/quot.lean

added theorem quotient.lift_beta

added theorem quotient.lift_on_beta

Created ring_theory/ideals.lean

added theorem is_maximal_ideal.mk

added def local_of_nonunits_ideal

added theorem mem_or_mem_of_mul_eq_zero

added theorem not_unit_of_mem_maximal_ideal

Created ring_theory/localization.lean

added def localization.at_prime

added def localization.away

added def localization.closure

added theorem localization.eq_zero_of_ne_zero_of_mul_eq_zero

added inductive localization.in_closure

added def localization.loc

added theorem localization.mem_non_zero_divisors_of_ne_zero

added theorem localization.ne_zero_of_mem_non_zero_divisors

added def localization.non_zero_divisors

added def localization.of_comm_ring

added def localization.quotient_ring.field.of_integral_domain

added def localization.quotient_ring

added def localization.r

added theorem localization.refl

added theorem localization.subset_closure

added theorem localization.symm

added theorem localization.trans