ker_single

Mathlib.LinearAlgebra.Pi

URI: https://scilib.ai/kg/mathlib#LinearMap.ker_single

English

The kernel of the i-th injection is trivial: ker(single R φ i) = ⊥.

Русский

Ядро инъекции в i-ю координату тривиально: ker(single R φ i) = ⊥.

LaTeX

$$$$\\ker\\bigl(\\text{single}_{R,\\varphi}(i)\\bigr) = \\{0\\}.$$$$

Lean4

theorem ker_single (i : ι) : ker (single R φ i) = ⊥ :=
  ker_eq_bot_of_injective <| Pi.single_injective _

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

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

Разделы

Аффилиация

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