Commit 2023-05-22 17:42 b8d6cde7

View on Github →

feat: port RingTheory.Localization.AsSubring (#4201)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/AsSubring.lean

added theorem Localization.mapToFractionRing_apply

added theorem Localization.map_isUnit_of_le

added theorem Localization.mem_range_mapToFractionRing_iff

added theorem Localization.subalgebra.mem_range_mapToFractionRing_iff_ofField