Commit 2024-06-05 11:47 8abdefba

View on Github →

chore: move the link between additive morphisms and linear maps earlier (#12457)

Estimated changes

Modified Mathlib/Algebra/Module/Equiv.lean

added def addMonoidEndRingEquivInt

added def addMonoidHomLequivInt

added def addMonoidHomLequivNat

Modified Mathlib/LinearAlgebra/Basic.lean

deleted def addMonoidEndRingEquivInt

deleted def addMonoidHomLequivInt

deleted def addMonoidHomLequivNat