trdeg_le_of_injective — Mathlib

English

If f: A →ₐ[R] A' is injective, then trdeg R A ≤ trdeg R A'.

Русский

Если f: A →ₐ[R] A' инъективно, то трэдгэд R A ≤ трэдгэд R A'.

LaTeX

$$$\\operatorname{trdeg}_R A \\le \\operatorname{trdeg}_R A'$$$

Lean4

theorem trdeg_le_of_injective {A' : Type v} [CommRing A'] [Algebra R A'] (f : A →ₐ[R] A') (hf : Injective f) :
    trdeg R A ≤ trdeg R A' := by rw [← (trdeg R A).lift_id, ← (trdeg R A').lift_id];
  exact lift_trdeg_le_of_injective f hf

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