Commit 2024-10-26 15:46 8cb7d6fc

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean

added def Ideal.quotEquivPowQuotPowSucc

added def Ideal.quotEquivPowQuotPowSuccEquiv

Modified Mathlib/RingTheory/Ideal/QuotientOperations.lean

added def Ideal.powQuotPowSuccEquivMapMkPowSuccPow

added def Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow