toDual_ker

Mathlib.LinearAlgebra.Dual.Basis

URI: https://scilib.ai/kg/mathlib#Module.Basis.toDual_ker

English

The kernel of the map toDual is trivial: ker(b.toDual) = ⊥.

Русский

Ядро отображения toDual тривиально: ker(b.toDual) = ⊥.

LaTeX

$$$ \ker(b.toDual) = \{0\} = \bot. $$$

Lean4

theorem toDual_ker : LinearMap.ker b.toDual = ⊥ :=
  ker_eq_bot'.mpr b.toDual_inj

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

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

Разделы

Аффилиация

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