Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-11 21:36 657df433

View on Github →

refactor(linear_algebra/tensor_product): make lift f (x ⊗ₜ y) = f x y true by rfl (#18121) Since this is essentially the "primitive" recursor, it is very convenient for it to expand definitionally. With this change, the following lemmas are now rfl:

  • algebra.mul'_apply
  • free_monoid.lift_comp_of
  • free_monoid.lift_eval_of
  • tensor_product.lie_module.lift_apply
  • alternating_map.dom_coprod'_apply
  • contract_left_apply
  • contract_right_apply
  • dual_tensor_hom_apply
  • derivation.tensor_product_to_tmul
  • poly_equiv_tensor.to_fun_linear_tmul_apply
  • tensor_product.lift.tmul
  • tensor_product.lift.tmul'
  • algebra.tensor_product.lift_tmul
  • algebra.tensor_product.lmul'_apply_tmul
  • tensor_product.algebra.smul_def And one lemma is no longer rfl
  • free_monoid.lift_apply

Estimated changes

modified theorem linear_map.mul'_apply
modified theorem free_monoid.lift_apply
modified theorem free_monoid.lift_comp_of
modified theorem free_monoid.lift_eval_of
modified theorem tensor_product.lift.tmul'
modified theorem tensor_product.lift.tmul