Commit 2024-08-14 10:13 d69f8430

View on Github →

chore: protect TensorProduct.{map_one, map_mul} (#15754) It's quite common to use the root ones, even with the TensorProduct namespace opened.

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

deleted theorem TensorProduct.map_mul

deleted theorem TensorProduct.map_one

Modified Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RingTheory/Bialgebra/Hom.lean

Modified Mathlib/RingTheory/Generators.lean

Modified Mathlib/RingTheory/IsTensorProduct.lean

Modified Mathlib/RingTheory/Kaehler/CotangentComplex.lean

Modified Mathlib/RingTheory/Presentation.lean

Modified Mathlib/RingTheory/Smooth/Kaehler.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean