Commit 2026-07-01 08:58 e5b7d955

View on Github →

feat(RingTheory/RamificationInertia/Inertia): add pow lemmas for new definition of inertia degree (#41215) This PR adds add pow lemmas for the new definition of inertia degree.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/ClassNumber.lean

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Galois.lean

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

Modified Mathlib/NumberTheory/NumberField/Discriminant/Different.lean

Modified Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

Modified Mathlib/RingTheory/RamificationInertia/Inertia.lean

added theorem Ideal.absNorm_pow_inertiaDeg'

added theorem Ideal.cardQuot_pow_inertiaDeg'

added theorem Ideal.natAbs_pow_inertiaDeg'

added theorem Ideal.pow_inertiaDeg'