Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-13 16:48 3a0ef3c2

View on Github →

feat(ring_theory): (strict) monotonicity of coe_submodule (#8273)

Estimated changes

Modified src/ring_theory/localization.lean

added theorem is_fraction_ring.coe_submodule_le_coe_submodule

added theorem is_fraction_ring.coe_submodule_strict_mono

added theorem is_localization.coe_submodule_le_coe_submodule

added theorem is_localization.coe_submodule_mono

added theorem is_localization.coe_submodule_strict_mono