Commit 2026-03-05 06:33 f5e1ab1d
View on Github →feat(RingTheory): base change of graded algebra (#30322)
In this file we show that if 𝒜 is a graded R-algebra, and S is any R-algebra, then S ⊗[R] 𝒜 (which is actually fun i ↦ (𝒜 i).baseChange S) is a graded S-algebra with the same grading.