Theorem Ideal.quotientToQuotientRangePowQuotSucc_injective

Modification history

2024-03-27 11:32

Mathlib/NumberTheory/RamificationInertia.lean

feat(DedekindDomain.Ideal): remove Domain assumption from DedekindDomain (#11527) …

Modified Ideal.quotientToQuotientRangePowQuotSucc_injective View on Github →

2023-06-08 06:34

Mathlib/NumberTheory/RamificationInertia.lean

feat: port NumberTheory.RamificationInertia (#4795)

Added Ideal.quotientToQuotientRangePowQuotSucc_injective View on Github →