Theorem Module.End.natCast_apply

Modification history

2024-02-02 13:15

Mathlib/Algebra/Module/LinearMap/Basic.lean

chore(Algebra/Module/LinearMap): split into 3 files (#10183)

Modified Module.End.natCast_apply View on Github →

2023-01-23 11:54

Mathlib/Algebra/Module/LinearMap.lean

fix: undo accidental rename from End to EndCat (#1778) …

Added Module.End.natCast_apply View on Github →