Def Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero

Modification history

2024-08-07 13:48
Mathlib/NumberTheory/RamificationInertia.lean
chore: backports for leanprover/lean4#4814 (part 26) (#15538)
Modified Ideal.Quotient.algebraQuotientOfRamificationIdxNeZeroView on Github →
2023-06-08 06:34
Mathlib/NumberTheory/RamificationInertia.lean
feat: port NumberTheory.RamificationInertia (#4795)
Added Ideal.Quotient.algebraQuotientOfRamificationIdxNeZeroView on Github →