coe_polyEquivTensor' — Mathlib

English

The coe of polyEquivTensor' equals coe of polyEquivTensor: the function parts coincide.

Русский

Коэффициентная карта polyEquivTensor' совпадает с polyEquivTensor: две функции совпадают.

LaTeX

$$⇑(polyEquivTensor' R A) = polyEquivTensor R A$$

Lean4

/-- `polyEquivTensor' R A` is the same as `polyEquivTensor R A` as a function. -/
@[simp]
theorem coe_polyEquivTensor' : ⇑(polyEquivTensor' R A) = polyEquivTensor R A :=
  rfl

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