isTranscendenceBasis_subtype_range

English

For an injective f, IsTranscendenceBasis R Subtype.val is equivalent to IsTranscendenceBasis R f.

Русский

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

LaTeX

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

Lean4

theorem isTranscendenceBasis_subtype_range {ι} {f : ι → A} (hf : Injective f) :
    IsTranscendenceBasis R ((↑) : range f → A) ↔ IsTranscendenceBasis R f :=
  .symm <| isTranscendenceBasis_equiv' (Equiv.ofInjective f hf) rfl

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