exists_isTranscendenceBasis' — Mathlib

English

If there exists a faithful R-action on A, there are an index type ι and a map x : ι → A forming a transcendence basis of A over R.

Русский

Пусть имеется допустимый стенд над R на A; существует индексный тип ι и отображение x:ι→A, образующие базис трансцендентности A над R.

LaTeX

$$$\exists (\iota : Type) \ (x : \iota \to A), IsTranscendenceBasis R x$$$

Lean4

/-- `Type` version of `exists_isTranscendenceBasis`. -/
theorem exists_isTranscendenceBasis' [FaithfulSMul R A] : ∃ (ι : Type w) (x : ι → A), IsTranscendenceBasis R x :=
  have ⟨s, h⟩ := exists_isTranscendenceBasis R A
  ⟨s, Subtype.val, h⟩

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