Commit 2025-11-09 18:05 3ac39f1c

View on Github →

refactor(NumberTheory/RamificationInertia/Galois): switch to IsGaloisGroup G A B (#30934) This PR cleans up the statements in NumberTheory/RamificationInertia/Galois by switching over to IsGaloisGroup G A B.

Estimated changes

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

Modified Mathlib/NumberTheory/NumberField/Basic.lean

Modified Mathlib/NumberTheory/NumberField/ClassNumber.lean

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

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

deleted theorem Ideal.exists_map_eq_of_isGalois

added theorem Ideal.exists_smul_eq_of_isGaloisGroup

modified theorem Ideal.inertiaDegIn_eq_inertiaDeg

modified theorem Ideal.inertiaDegIn_ne_zero

deleted theorem Ideal.inertiaDeg_eq_of_isGalois

added theorem Ideal.inertiaDeg_eq_of_isGaloisGroup

deleted theorem Ideal.isPretransitive_of_isGalois

modified theorem Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn

modified theorem Ideal.ramificationIdxIn_eq_ramificationIdx

deleted theorem Ideal.ramificationIdx_eq_of_isGalois

added theorem Ideal.ramificationIdx_eq_of_isGaloisGroup

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

Modified Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean

added theorem integralClosure.coe_smul

Modified Mathlib/RingTheory/Invariant/Basic.lean