Commit 2021-08-16 16:19 65b0c582

View on Github →

feat(ring_theory/localization): some lemmas on coe_submodule (#8621) A small assortment of results on is_localization.coe_submodule, needed for elementary facts about the ideal class group.

Estimated changes

Modified src/ring_theory/localization.lean

added theorem is_fraction_ring.coe_submodule_injective

added theorem is_fraction_ring.coe_submodule_is_principal

added theorem is_localization.coe_submodule_injective

added theorem is_localization.coe_submodule_is_principal

added theorem is_localization.coe_submodule_span

added theorem is_localization.coe_submodule_span_singleton