algebraicIndependent_subtype_range

English

IsTranscendenceBasis R Subtype.val is equivalent to IsTranscendenceBasis R f for an injective f.

Русский

IsTranscendenceBasis R Subtype.val эквивалентно IsTranscendenceBasis R f для инъективного f.

LaTeX

$$$\\text{IsTranscendenceBasis } R\\, (\\mathrm{Subtype}.val) \\iff \\text{IsTranscendenceBasis } R\\, f$$$

Lean4

theorem algebraicIndependent_subtype_range {ι} {f : ι → A} (hf : Injective f) :
    AlgebraicIndependent R ((↑) : range f → A) ↔ AlgebraicIndependent R f :=
  Iff.symm <| algebraicIndependent_equiv' (Equiv.ofInjective f hf) rfl

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