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) …

Added IsLocalization.AtPrime.nontrivial View on Github →