Def Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero

Modification history

2024-12-10 15:20
Mathlib/NumberTheory/RamificationInertia/Basic.lean
refactor/fix: don't use RingHom.toAlgebra in Ideal.quotientAlgebra (#19847)
Modified Ideal.Quotient.algebraQuotientOfRamificationIdxNeZeroView on Github →
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 →