matroid — Mathlib

English

The cardinal rank associated with the algebraic independent matroid equals the transcendence degree.

Русский

Кардинальный ранг матроида алгебраической независимости равен трансцендентному размеру.

LaTeX

$$$ (matroid R A).cRank = \operatorname{trdeg} R A $$$

Lean4

/-- If `R` is a commutative ring and `A` is a commutative `R`-algebra with injective algebra map
and no zero-divisors, then the `R`-algebraic independent subsets of `A` form a matroid. -/
def matroid : Matroid A :=
  (indepMatroid R A).matroid.copyBase univ (fun s ↦ IsTranscendenceBasis R ((↑) : s → A)) rfl
    (fun B ↦ by simp_rw [Matroid.isBase_iff_maximal_indep, isTranscendenceBasis_iff_maximal]; rfl)

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