Theorem IsPrincipalIdealRing.of_surjective

Modification history

2024-10-22 08:37

Mathlib/RingTheory/PrincipalIdealDomain.lean

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

Modified IsPrincipalIdealRing.of_surjective View on Github →

2023-03-21 11:38

Mathlib/RingTheory/PrincipalIdealDomain.lean

feat: port RingTheory.PrincipalIdealDomain (#3012)

Added IsPrincipalIdealRing.of_surjective View on Github →