Theorem Ideal.IsPrincipal.of_comap

Modification history

2024-10-22 08:37

Mathlib/RingTheory/PrincipalIdealDomain.lean

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

Modified Ideal.IsPrincipal.of_comap View on Github →

2023-03-21 11:38

Mathlib/RingTheory/PrincipalIdealDomain.lean

feat: port RingTheory.PrincipalIdealDomain (#3012)

Added Ideal.IsPrincipal.of_comap View on Github →