restrictScalars_rTensor — Mathlib

English

For any map f : M →_A P, the coerced RTensor equals the canonical rTensor: coe_rTensor (f) = f.rTensor N.

Русский

Для отображения f : M →_A P ковариантная версия RTensor совпадает с каноническим rTensor: coe_rTensor (f) = f.rTensor N.

LaTeX

$$$(\text{coe}_{{\!}rTensor}\; f) = f.rTensor N$$$

Lean4

@[simp]
theorem restrictScalars_rTensor (f : M →ₗ[A] P) : (rTensor R N f).restrictScalars R = f.rTensor N :=
  rfl

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