range_restrictScalars — Mathlib

English

As above: range f ≤ p iff comap f p = ⊤.

Русский

Как выше: range f ≤ p тогда и только тогда, когда comap f p = ⊤.

LaTeX

$$$\operatorname{range} f \le p \iff \operatorname{comap} f p = \top$$$

Lean4

theorem range_restrictScalars [SMul R R₂] [Module R₂ M] [Module R M₂] [CompatibleSMul M M₂ R R₂] [IsScalarTower R R₂ M₂]
    (f : M →ₗ[R₂] M₂) : LinearMap.range (f.restrictScalars R) = (LinearMap.range f).restrictScalars R :=
  rfl

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