Commit 2026-10-08 13:29 9304843e

chore: weaken hypotheses of Algebra.IsUnramifiedIn.ramificationIdx_eq_one (#41578) This PR drops the unused [IsDomain R] [Module.Finite ℤ R] [CharZero R] [Algebra.IsIntegral R S] hypotheses from Algebra.IsUnramifiedIn.ramificationIdx_eq_one by proving via Ideal.ramificationIdx_eq_one directly rather than through Ideal.ramificationIdx_eq_one_iff, and tidy the docstrings in Mathlib/RingTheory/Unramified/Locus.lean (fix a stray space before a period, mention Algebra.IsUnramifiedIn in the module docstring, add a missing blank line). Follow-up to [#40886 (feat: add Algebra.IsUnramifiedIn)](https://github.com/leanprover-community/mathlib4/pull/40886). 🤖 Prepared with Claude Code