Def Ideal.quotEquivPowQuotPowSucc

Modification history

2025-05-01 12:28

Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean

chore: whitespace still (#24501) …

Modified Ideal.quotEquivPowQuotPowSucc View on Github →

2024-10-26 15:46

Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean

feat(Ideal/IsPrincipalPowQuotient): R/I equiv I^n/I^(n+1) (#15426)

Added Ideal.quotEquivPowQuotPowSucc View on Github →