Commit 2026-03-17 11:40 a47bc60f

View on Github →

chore(Algebra): make TensorProduct.equivOfCompatibleSMul more linear (#35643)

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Associator.lean

added theorem TensorProduct.CompatibleSMul.of_algebraMap_surjective

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

modified def TensorProduct.equivOfCompatibleSMul

deleted def TensorProduct.mapOfCompatibleSMul'

modified def TensorProduct.mapOfCompatibleSMul

modified theorem TensorProduct.mapOfCompatibleSMul_surjective

modified theorem TensorProduct.mapOfCompatibleSMul_tmul

Modified Mathlib/RingTheory/Coalgebra/TensorProduct.lean

Modified Mathlib/RingTheory/LinearDisjoint.lean

Modified Mathlib/RingTheory/Localization/BaseChange.lean

Modified Mathlib/RingTheory/Smooth/Fiber.lean

Modified Mathlib/RingTheory/TensorProduct/Maps.lean

modified def Algebra.TensorProduct.equivOfCompatibleSMul

deleted def Algebra.TensorProduct.mapOfCompatibleSMul'

modified def Algebra.TensorProduct.mapOfCompatibleSMul

modified theorem Algebra.TensorProduct.mapOfCompatibleSMul_surjective

modified theorem Algebra.TensorProduct.mapOfCompatibleSMul_tmul

Modified Mathlib/RingTheory/TensorProduct/Nontrivial.lean