Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-29 14:43 ca5176c3

View on Github →

feat(linear_algebra/tensor_product): add definition tensor_product.map_incl and simp lemmas related to powers of tensor_product.map (#7406)

Estimated changes

added theorem linear_map.id_pow
modified theorem linear_map.ltensor_id
added theorem linear_map.ltensor_pow
modified theorem linear_map.rtensor_id
added theorem linear_map.rtensor_pow
added theorem tensor_product.map_id
added theorem tensor_product.map_mul
added theorem tensor_product.map_one
added theorem tensor_product.map_pow