Commit 2025-08-21 12:13 295a40f0
View on Github →chore(RingTheory/Generators): make type argument in localizationAway
and baseChange
explicit (#28697)
The S
(resp. T
) argument in Generators.localizationAway
(resp. Generators.baseChange
) is not inferable from the other arguments and is currently frequently explicitly provided.
Moreover, Presentation.localizationAway
(resp. Presentation.baseChange
) already take S
(resp. T
) explicitly.