repr_ker

Mathlib.LinearAlgebra.LinearIndependent.Defs

URI: https://scilib.ai/kg/mathlib#LinearIndependent.repr_ker

English

The kernel of the repr map is trivial; it is the zero subspace.

Русский

Ядро отображения repr тривиально; это нулевой подпространство.

LaTeX

$$$\\operatorname{ker}(hv.repr) = \\{0\\}$$$

Lean4

theorem repr_ker : LinearMap.ker hv.repr = ⊥ := by rw [LinearIndependent.repr, LinearEquiv.ker]

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

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

Разделы

Аффилиация

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