flag_zero

Mathlib.LinearAlgebra.Basis.Flag

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

English

Basis.finTwoProd R 0 equals (1,0).

Русский

Basis.finTwoProd R 0 равно (1,0).

LaTeX

$$$\text{Basis.finTwoProd } R\ 0 = (1,0)$$$

Lean4

@[simp]
theorem flag_zero (b : Basis (Fin n) R M) : b.flag 0 = ⊥ := by simp [flag]

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

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

Разделы

Аффилиация

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