exists_isTranscendenceBasis — Mathlib

English

Assuming a faithful scalar action of R on A, there exists a subset s of A that forms a transcendence basis of A over R.

Русский

Пусть действует над A безошибочно R–скаляры; существует множество s ⊆ A, образующее базис трансцендентности A над R.

LaTeX

$$$\exists s:\ Set A, IsTranscendenceBasis R ((\uparrow) : s \to A)$$$

Lean4

theorem exists_isTranscendenceBasis [FaithfulSMul R A] : ∃ s : Set A, IsTranscendenceBasis R ((↑) : s → A) := by
  simpa using
    exists_isTranscendenceBasis_superset
      ((algebraicIndependent_empty_iff R A).mpr (FaithfulSMul.algebraMap_injective R A))

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