of_comp_algebraMap — Mathlib

English

If H is IsTranscendenceBasis R x then IsTranscendenceBasis R (Function.comp (algebraMap A A') x).

Русский

Если H является IsTranscendenceBasis R x, то IsTranscendenceBasis R (algebraMap A A' ∘ x).

LaTeX

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

Lean4

theorem of_comp_algebraMap [Algebra A A'] [IsScalarTower R A A'] [FaithfulSMul A A'] {x : ι → A}
    (H : IsTranscendenceBasis R (algebraMap A A' ∘ x)) : IsTranscendenceBasis R x :=
  .of_comp (IsScalarTower.toAlgHom R A A') (FaithfulSMul.algebraMap_injective A A') H

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