Theorem Algebra.TensorProduct.restrictScalars_lift

Modification history

2026-05-01 19:07
Mathlib/RingTheory/TensorProduct/Maps.lean
refactor(Localization/AtPrime/Basic): add predicate for algebra instance on `Localization.AtPrime` (#38465) …
Added Algebra.TensorProduct.restrictScalars_liftView on Github →