Commit 2024-10-22 08:37 b2cf5147

View on Github →

chore(RingTheory/PrincipalIdealDomain): factor out IsPrincipal.map, use RingHomClass (#18010)

Estimated changes

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

modified theorem Ideal.IsPrincipal.of_comap

modified theorem IsPrincipalIdealRing.of_surjective

added theorem Submodule.IsPrincipal.map

added theorem Submodule.IsPrincipal.map_ringHom