isTranscendenceBasis_iff_of_subsingleton

English

For a subsingleton R, IsTranscendenceBasis R x iff Nonempty ι.

Русский

Пусть R сводимо к едва ли не единственному элементу; тогда IsTranscendenceBasis R x эквивалентно не пустоте множества индексов ι.

LaTeX

$$$\\mathrm{IsTB}_R(x) \\;\\iff\\; ι \\neq \\varnothing$$$

Lean4

theorem isTranscendenceBasis_iff_of_subsingleton [Subsingleton R] (x : ι → A) : IsTranscendenceBasis R x ↔ Nonempty ι :=
  by
  have := Module.subsingleton R A
  refine
    ⟨fun h ↦ ?_, fun h ↦
      ⟨.of_subsingleton, fun s hs hx ↦ hx.antisymm fun a _ ↦ ⟨Classical.arbitrary _, Subsingleton.elim ..⟩⟩⟩
  by_contra! hι
  have := h.2 {0} .of_subsingleton
  simp [range_eq_empty, eq_comm (a := ∅)] at this

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