isTranscendenceBasis — Mathlib

English

If e is an algebra equivalence, IsTranscendenceBasis R x implies IsTranscendenceBasis R (e ∘ x).

Русский

Если e — алгебраическое эквивалентство, то IsTranscendenceBasis R x влечёт IsTranscendenceBasis R (e ∘ x).

LaTeX

$$$\\mathrm{AlgEquivIsTB}(e)\\_R(x) \\Rightarrow \\mathrm{IsTB}_R(e \\circ x)$$$

Lean4

/-- Also see `IsTranscendenceBasis.algebraMap_comp`
for the composition with a algebraic extension. -/
theorem isTranscendenceBasis (e : A ≃ₐ[R] A') (hx : IsTranscendenceBasis R x) : IsTranscendenceBasis R (e ∘ x) :=
  .of_comp e.symm.toAlgHom e.symm.injective (by convert hx; ext; simp)

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