Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-10-11 09:58
9ff5b6f1
View on Github →
feat: use suppress_compilation in tensor products (
#7504
) More principled version of
#7281
.
Estimated changes
Modified
Mathlib/Algebra/Algebra/Bilinear.lean
deleted
def
LinearMap.mul'
Modified
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
Modified
Mathlib/Algebra/Category/Ring/Constructions.lean
Modified
Mathlib/Algebra/Lie/BaseChange.lean
Modified
Mathlib/Algebra/Lie/TensorProduct.lean
Modified
Mathlib/Algebra/Lie/Weights.lean
Modified
Mathlib/AlgebraicGeometry/Limits.lean
Modified
Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
Modified
Mathlib/Data/Matrix/Kronecker.lean
Modified
Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
Modified
Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
Modified
Mathlib/LinearAlgebra/Contraction.lean
Modified
Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
Modified
Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean
Modified
Mathlib/LinearAlgebra/PiTensorProduct.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean
Modified
Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
Modified
Mathlib/LinearAlgebra/TensorPower.lean
Modified
Mathlib/LinearAlgebra/TensorProduct.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Opposite.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Prod.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Tower.lean
Modified
Mathlib/RepresentationTheory/Basic.lean
deleted
def
Representation.tprod
Modified
Mathlib/RepresentationTheory/FdRep.lean
Modified
Mathlib/RepresentationTheory/Invariants.lean
Modified
Mathlib/RepresentationTheory/Rep.lean
Modified
Mathlib/RingTheory/Finiteness.lean
Modified
Mathlib/RingTheory/Kaehler.lean
Modified
Mathlib/RingTheory/MatrixAlgebra.lean
Modified
Mathlib/RingTheory/TensorProduct.lean
Modified
Mathlib/Tactic/SuppressCompilation.lean
added
def
expandSuppressCompilationNotation