Commit 2025-08-22 15:25 a3e995e2

View on Github →

feat(RingTheory/Coalgebra/MulOpposite): coalgebra instance for MulOpposite (#25858) Adding an instance for Aᵐᵒᵖ being an R-coalgebra when A is.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem LinearMap.lTensor_map

added theorem LinearMap.map_lTensor

added theorem LinearMap.map_rTensor

added theorem LinearMap.rTensor_map

Created Mathlib/RingTheory/Coalgebra/MulOpposite.lean

added theorem MulOpposite.comul_def

added theorem MulOpposite.counit_def