Theorem IsDedekindDomain.exists_add_spanSingleton_mul_eq

Modification history

2025-06-14 13:55
Mathlib/RingTheory/DedekindDomain/Factorization.lean
feat(NumberTheory): discriminant is norm of different (#25792)
Added IsDedekindDomain.exists_add_spanSingleton_mul_eqView on Github →