Commit 2025-03-24 00:15 5c2583ab
View on Github →chore: deprecate duplicate lemma isAlgebraic_of_isLocalization (#23237)
Deprecates isAlgebraic_of_isLocalization, which was added in 2a950180fd7e49c4a374c7595d858eed58573afc, in favor of IsLocalization.isAlgebraic, which was added more recently, in ea266590e7c060ee0e5a7fa6a95966304975e019.
These lemmas have the same signatures, modulo ordering of parameters.
This duplication was found by tryAtEachStep.