Commit 2026-08-05 02:09 2eecc3c0

View on Github →

chore(Algebra/Module/Equiv/Basic): fix lemma name (#42441)

Estimated changes

Modified Mathlib/Algebra/Module/Equiv/Basic.lean

deleted theorem LinearEquiv.ofLinear_toLinearMap

added theorem LinearEquiv.toLinearMap_ofLinearMap

Modified Mathlib/RingTheory/Coalgebra/Equiv.lean