Commit 2025-08-01 13:45 cf9cfce8
View on Github →chore(RingTheory/Localization/AtPrime): rename AtPrime.Nontrivial to AtPrime.nontrivial (#27798)
This is more in line with the naming convention and otherwise defining a nontrivial instance when the namespace IsLocalization.AtPrime is open causes an error.