isTranscendenceBasis_equiv' — Mathlib

English

If h is an equality f ∘ e = g, then IsTranscendenceBasis R g ↔ IsTranscendenceBasis R f.

Русский

Если f ∘ e = g, то IsTranscendenceBasis R g ↔ IsTranscendenceBasis R f.

LaTeX

$$$f \\circ e = g \\Rightarrow IsTranscendenceBasis R g \\iff IsTranscendenceBasis R f$$$

Lean4

theorem isTranscendenceBasis_equiv' (e : ι ≃ ι') {f : ι' → A} {g : ι → A} (h : f ∘ e = g) :
    IsTranscendenceBasis R g ↔ IsTranscendenceBasis R f :=
  h ▸ isTranscendenceBasis_equiv e

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