Theorem Submodule.IsPrincipal.map_ringHom

Modification history

2024-10-22 08:37

Mathlib/RingTheory/PrincipalIdealDomain.lean

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

Added Submodule.IsPrincipal.map_ringHom View on Github →