coe_linearEquivTuple_symm — Mathlib

English

The underlying function of the linear equivalence linearEquivTuple is equal to the underlying function of the corresponding equivalence equivTuple.

Русский

Элемент линейного эквивалента linearEquivTuple имеет ту же обобщённую композицию функций, что и эквивалентность equivTuple.

LaTeX

$$$\operatorname{toFun} (linearEquivTuple\, c_{1}\, c_{2}\, c_{3}) = \operatorname{toFun} (equivTuple\, c_{1}\, c_{2}\, c_{3}).$$$

Lean4

@[simp]
theorem coe_linearEquivTuple_symm : ⇑(linearEquivTuple c₁ c₂ c₃).symm = (equivTuple c₁ c₂ c₃).symm :=
  rfl

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