Commit 2023-04-18 05:52 3e6e0fe4

View on Github →

feat: port RingTheory.Localization.Ideal (#3452)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/Ideal.lean

added theorem IsLocalization.bot_lt_comap_prime

added theorem IsLocalization.comap_map_of_isPrime_disjoint

added theorem IsLocalization.isPrime_iff_isPrime_disjoint

added theorem IsLocalization.isPrime_of_isPrime_disjoint

added theorem IsLocalization.map_comap

added theorem IsLocalization.mem_map_algebraMap_iff

added def IsLocalization.orderEmbedding

added def IsLocalization.orderIsoOfPrime

added theorem IsLocalization.surjective_quotientMap_of_maximal_of_localization