Commit 2023-01-23 11:54 99815145

View on Github →

fix: undo accidental rename from End to EndCat (#1778) Also fixes some names in docstrings

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap.lean

modified def DistribMulAction.toModuleEnd

modified theorem LinearMap.coe_mul

modified theorem LinearMap.coe_one

modified theorem LinearMap.mul_apply

modified theorem LinearMap.mul_eq_comp

modified theorem LinearMap.one_apply

modified theorem LinearMap.one_eq_id

added theorem Module.End.intCast_apply

added theorem Module.End.intCast_def

added theorem Module.End.natCast_apply

added theorem Module.End.natCast_def

deleted theorem Module.EndCat.intCast_apply

deleted theorem Module.EndCat.intCast_def

deleted theorem Module.EndCat.natCast_apply

deleted theorem Module.EndCat.natCast_def

modified def Module.moduleEndSelf

modified def Module.moduleEndSelfOp

modified def Module.toModuleEnd