Theorem IsLocalization.mk'_eq_algebraMap_mk'_of_submonoid_le

Modification history

2024-09-16 11:07
Mathlib/RingTheory/Localization/LocalizationLocalization.lean
feat(RingTheory/IntegralClosure/IntegrallyClosed): `IsIntegrallyClosed` is a local property (#16558) …
Added IsLocalization.mk'_eq_algebraMap_mk'_of_submonoid_leView on Github →