Theorem Ideal.exists_smul_eq_of_isGaloisGroup

Modification history

2025-11-09 18:05
Mathlib/NumberTheory/RamificationInertia/Galois.lean
refactor(NumberTheory/RamificationInertia/Galois): switch to `IsGaloisGroup G A B` (#30934) …
Added Ideal.exists_smul_eq_of_isGaloisGroupView on Github →