Commit 2026-06-22 15:26 cba41737

View on Github →

feat: add Algebra.IsUnramifiedIn (#40886)

Estimated changes

Modified Mathlib/NumberTheory/RamificationInertia/Unramified.lean

modified theorem Algebra.IsUnramifiedAt.of_liesOver

added theorem Algebra.IsUnramifiedIn.ramificationIdx_eq_one

added theorem Algebra.isUnramifiedAt_bot

modified theorem Algebra.isUnramifiedAt_iff_of_isDedekindDomain

added theorem Algebra.isUnramifiedIn_bot

added theorem Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain'

added theorem Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain

added theorem Algebra.isUnramifiedIn_iff_forall_ramificationIdx_eq_one

Modified Mathlib/RingTheory/Unramified/Locus.lean

added def Algebra.IsUnramifiedIn

added theorem Algebra.isUnramifiedIn_top