Commit 2025-12-31 12:47 78ce4854

View on Github →

feat: transfer Coalgebra.IsCocomm across an Equiv (#33139) ... and generalise the existing tensorProductAssoc_def to be about possibly several transferred instances.

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Associator.lean

modified theorem Equiv.tensorProductAssoc_def

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem Equiv.tensorProductComm_def

Modified Mathlib/RingTheory/Coalgebra/Basic.lean

added theorem Equiv.coalgebraIsCocomm