Theorem NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply

Modification history

2025-09-16 15:34
Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean
feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers (#26101) …
Added NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_applyView on Github →