operations): add lemmas about comap (#10418)

Commit

4 years ago

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

Author

eric-wieser

Parents