coe_toIntLinearMap_range — Mathlib

English

Restricting the codomain scalars preserves the range: range_restrictScalars f = range f restricted to the same scalars.

Русский

Ограничение скаляров кодомапа сохраняет диапазон: range_restrictScalars f = range f с теми же скалярами.

LaTeX

$$$\operatorname{range}(f.\mathrm{restrictScalars} R) = (\operatorname{range} f).\restrictScalars R$$$

Lean4

@[simp]
theorem _root_.AddMonoidHom.coe_toIntLinearMap_range {M M₂ : Type*} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :
    LinearMap.range f.toIntLinearMap = AddSubgroup.toIntSubmodule f.range :=
  rfl

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