finrank_empty

Mathlib.LinearAlgebra.Dimension.Finite

URI: https://scilib.ai/kg/mathlib#Set.finrank_empty

English

The finrank of the empty set is zero.

Русский

Финранк пустого множества равен нулю.

LaTeX

$$$$\\\\operatorname{finrank}_R(\\\\emptyset) = 0.$$$$

Lean4

@[simp]
theorem finrank_empty [Nontrivial R] : Set.finrank R (∅ : Set M) = 0 := by rw [Set.finrank, span_empty, finrank_bot]

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

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

Разделы

Аффилиация

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