Commit 2025-10-27 15:02 0cf8d72a

View on Github →

chore(RingTheory/TensorProduct/Basic): split RingTheory.TensorProduct.Basic (#30806) This PR splits the file

  • Mathlib/RingTheory/TensorProduct/Basic.lean into
  • Mathlib/RingTheory/TensorProduct/Basic.lean
  • Mathlib/RingTheory/TensorProduct/Maps.lean Everything from the file Basic.lean related to maps between tensor products of R-algebras has been moved to a new file Maps.lean, unless it is required for constructions.

Estimated changes