ker_mapRange

Mathlib.LinearAlgebra.Finsupp.Pi

URI: https://scilib.ai/kg/mathlib#Finsupp.ker_mapRange

← MathLib Explorer

English

A simp lemma for ker_mapRange simplifying the kernel description.

Русский

Упрощающее лемма для ker_mapRange.

LaTeX

$$$\ker (mapRange.linearMap f) = \{ x \mid \forall i, x_i \in \ker f\}$$$

Lean4

theorem ker_mapRange (f : M →ₗ[R] N) (I : Type*) :
    LinearMap.ker (mapRange.linearMap (α := I) f) = submodule (fun _ => LinearMap.ker f) :=
  by
  ext x
  simp [Finsupp.ext_iff]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru