Commit 2025-07-02 08:48 5ac55175
View on Github →feat(RingTheory): lemmas about TensorProduct and IsBaseChange (#26297)
Add lemmas about TensorProduct and IsBaseChange.
These are used to prove that RingTheory.Sequence.IsWeaklyRegular is stable under flat base change and RingTheory.Sequence.IsRegular is stable under faithfully flat base change.