Commit 2026-10-07 11:50 6e304baf

View on Github →

chore: rename unramifedPlacesOver_ncard_add_eq_finrank to unramifiedPlacesOver_ncard_add_eq_finrank (#44522) Fixes the misspelling unramifed to match unramifiedPlacesOver. 🤖 Generated with Claude Code

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Completion/Ramification.lean

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

deleted theorem NumberField.InfinitePlace.unramifedPlacesOver_ncard_add_eq_finrank

added theorem NumberField.InfinitePlace.unramifiedPlacesOver_ncard_add_eq_finrank