dualTensorHomEquivOfBasis_symm_cancel_left

English

The symmetrized inverse of the basis-equivalence cancels on the left in a simple way.

Русский

Симметричная обратная базисная эквивалентность снимается слева простым образом.

LaTeX

$$$(dualTensorHomEquivOfBasis b).symm (dualTensorHom R M N x) = x$$$

Lean4

@[simp]
theorem dualTensorHomEquivOfBasis_symm_cancel_left (x : Module.Dual R M ⊗[R] N) :
    (dualTensorHomEquivOfBasis b).symm (dualTensorHom R M N x) = x := by
  rw [← dualTensorHomEquivOfBasis_apply b, LinearEquiv.symm_apply_apply <| dualTensorHomEquivOfBasis (N := N) b]

Похожие утверждения