ker_eq_bot

Mathlib.LinearAlgebra.BilinearForm.Properties

URI: https://scilib.ai/kg/mathlib#LinearMap.BilinForm.Nondegenerate.ker_eq_bot

English

Nondegenerate B is equivalent to ker B = ⊥.

Русский

Недеформируемость B эквивалентна ker B = ⊥.

LaTeX

$$$B.Nondegenerate \\iff LinearMap.ker B = ⊥$$$

Lean4

theorem ker_eq_bot {B : BilinForm R M} (h : B.Nondegenerate) : LinearMap.ker B = ⊥ :=
  nondegenerate_iff_ker_eq_bot.mp h

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

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

Разделы

Аффилиация

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