Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-02 02:22 f63069f3

View on Github →

feat(linear_algebra/basic): simp lemmas about endomorphisms (#6452) Also renames some lemmas:

  • linear_map.one_app has been renamed to linear_map.one_apply
  • linear_map.mul_app has been removed in favour of the existing linear_map.mul_app.

Estimated changes

added theorem linear_map.coe_mul
added theorem linear_map.coe_one
added theorem linear_map.coe_pow
deleted theorem linear_map.mul_app
modified theorem linear_map.mul_apply
deleted theorem linear_map.one_app
added theorem linear_map.one_apply
added theorem linear_map.pow_apply