Commit 2025-08-19 04:15 52b282e3
View on Github →feat(RingTheory/IntegralClosure/Algebra/Basic): Move IsIntegral.tmul and Algebra.IsIntegral.tensorProduct (#28207)
This PR moves IsIntegral.tmul and Algebra.IsIntegral.tensorProduct from Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean to Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean.