trdeg_add_eq — Mathlib

English

Under the standard setup, trdeg R S + trdeg S A = trdeg R A.

Русский

В стандартной постановке trdeg R S + trdeg S A = trdeg R A.

LaTeX

$$$trdeg R S + trdeg S A = trdeg R A$$

Lean4

@[stacks 030H]
theorem trdeg_add_eq [Nontrivial R] {A : Type v} [CommRing A] [NoZeroDivisors 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_eq R S A

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