Commit 2023-11-08 15:00 5c17a3a9

View on Github →

chore(Topology/Algebra/Module/Basic): missing cast lemmas and better defeq (#8267)

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap.lean

added theorem Module.End.ofNat_apply

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

added theorem ContinuousLinearMap.algebraMap_apply

added theorem ContinuousLinearMap.intCast_apply

added theorem ContinuousLinearMap.natCast_apply

added theorem ContinuousLinearMap.ofNat_apply