isTranscendenceBasis_iff_maximal — Mathlib

English

IsTranscendenceBasis R ((↑) : s → A) holds iff s is a maximal set with respect to AlgebraicIndepOn R id.

Русский

IsTranscendenceBasis R ((↑): s → A) эквивалентно тому, что s является максимальным с точки зрения AlgebraicIndepOn R id.

LaTeX

$$$\\text{IsTranscendenceBasis } R ((\\uparrow) : s \\to A) \\iff \\text{Maximal } (\\text{AlgebraicIndepOn } R id)\\ s$$

Lean4

theorem isTranscendenceBasis_iff_maximal {s : Set A} :
    IsTranscendenceBasis R ((↑) : s → A) ↔ Maximal (AlgebraicIndepOn R id) s := by
  rw [IsTranscendenceBasis, maximal_iff, Subtype.range_val]; rfl

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