Theorem IsLocalization.AtPrime.Nontrivial
Modification history
2025-08-01 13:45
Mathlib/RingTheory/Localization/AtPrime.lean
chore(RingTheory/Localization/AtPrime): rename `AtPrime.Nontrivial` to `AtPrime.nontrivial` (#27798) …
Deleted IsLocalization.AtPrime.NontrivialView on Github →