Theorem KummerDedekind.quotMapEquivQuotQuotMap_symm_apply

Modification history

2025-06-03 18:34
Mathlib/NumberTheory/KummerDedekind.lean
feat(NumberTheory.KummerDedekind): add more results about the conductor of an algebraic integer (#25316) …
Added KummerDedekind.quotMapEquivQuotQuotMap_symm_applyView on Github →