Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-26 16:19 ea52ec1f

View on Github →

feat(ring_theory/ideal/operations): add lemmas about comap (#10418) This also adds ring_hom.to_semilinear_map and ring_equiv.to_semilinear_equiv.

Estimated changes

Modified src/algebra/module/linear_map.lean

added def ring_hom.to_semilinear_map

Modified src/data/equiv/module.lean

added def ring_equiv.to_semilinear_equiv

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.comap_le_map_of_inv_on

added theorem ideal.comap_le_map_of_inverse

added theorem ideal.map_le_comap_of_inv_on

added theorem ideal.map_le_comap_of_inverse

added theorem ring_hom.comap_ker