Commit 2025-10-26 15:49 61d564ba

View on Github →

feat(NumberTheory): order of inertia group = ramification index (#30675)

Estimated changes

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

added theorem Ideal.card_inertia_eq_ramificationIdxIn

added theorem Ideal.ncard_primesOver_mul_card_inertia_mul_finrank

Modified Mathlib/RingTheory/Ideal/Over.lean

added theorem Ideal.Quotient.ker_stabilizerHom

added theorem Ideal.Quotient.map_ker_stabilizer_subtype

Modified Mathlib/RingTheory/Ideal/Pointwise.lean

added theorem Ideal.inertia_le_stabilizer