coe_restrictScalars' — Mathlib

English

The coercion from ContinuousLinearMap.restrictScalars to the underlying linear map is projection-equivalent to the identity on the base ring.

Русский

Переход от restrictScalars к базовой линейной карте эквивалентен тождественному отображению на базовом кольце.

LaTeX

$$$$ \text{coeLM}(f) = f $$$$

Lean4

@[simp]
theorem coe_restrictScalars' (f : M₁ →L[A] M₂) : ⇑(f.restrictScalars R) = f :=
  rfl

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