Theorem Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain

Modification history

2026-06-22 15:26
Mathlib/NumberTheory/RamificationInertia/Unramified.lean
feat: add Algebra.IsUnramifiedIn (#40886)
Added Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomainView on Github →