matroid_indep_iff — Mathlib

English

A subset is independent in the algebraic independent matroid if and only if it is algebraically independent over R when viewed as a subset.

Русский

Подмножество является независимым в этом матроиде тогда и только тогда, когда оно алгебраически независимо над R как подмножество.

LaTeX

$$$ (matroid R A).Indep s \iff AlgebraicIndepOn R id s$$$

Lean4

theorem matroid_indep_iff {s : Set A} : (matroid R A).Indep s ↔ AlgebraicIndepOn R id s :=
  Iff.rfl

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