Commit 2022-12-13 03:30 d8615108

View on Github →

feat(ring_theory/valuation/valuation_subring): Add valuation_subring.comap (#17310) Some definitions required for the definition of Frobenius elements.

Estimated changes

Modified src/ring_theory/subsemiring/basic.lean

added theorem ring_hom.coe_restrict_apply

added theorem ring_hom.comp_restrict

added def ring_hom.dom_restrict

modified def ring_hom.restrict

modified theorem ring_hom.restrict_apply

Modified src/ring_theory/valuation/valuation_subring.lean

added theorem valuation_subring.coe_comap

added def valuation_subring.comap

added theorem valuation_subring.comap_comap

added theorem valuation_subring.mem_comap