trdeg_add_le — Mathlib

English

For a tower of algebras with faithful scalar actions, the sum of trdeg’s is bounded by the trdeg over the base: trdeg R S + trdeg S A ≤ trdeg R A.

Русский

Для башни алгебр с верной скаляровой деформацией сумма степеней трансцендентности не превышает трансцендентность над основанием: trdeg R S + trdeg S A ≤ trdeg R A.

LaTeX

$$$\\mathrm{trdeg}\\,R S + \\mathrm{trdeg}\\,S A \\le \\mathrm{trdeg}\\,R A$$$

Lean4

theorem trdeg_add_le [Nontrivial R] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [FaithfulSMul R S]
    [FaithfulSMul S A] [IsScalarTower R S A] : trdeg R S + trdeg S A ≤ trdeg R A :=
  by
  rw [← (trdeg R S).lift_id, ← (trdeg S A).lift_id, ← (trdeg R A).lift_id]
  exact lift_trdeg_add_le

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