isTranscendenceBasis_equiv — Mathlib

English

IsTranscendenceBasis R (f ∘ e) ↔ IsTranscendenceBasis R f for an equivalence e.

Русский

IsTranscendenceBasis R (f ∘ e) ↔ IsTranscendenceBasis R f для эквивалентности e.

LaTeX

$$$IsTranscendenceBasis R (f \\circ e) \\iff IsTranscendenceBasis R f$$$

Lean4

theorem isTranscendenceBasis_equiv (e : ι ≃ ι') {f : ι' → A} :
    IsTranscendenceBasis R (f ∘ e) ↔ IsTranscendenceBasis R f := by
  simp_rw [IsTranscendenceBasis, algebraicIndependent_equiv, EquivLike.range_comp]

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