trdeg_eq_zero_of_not_injective — Mathlib

English

If the algebra map algebraMap R A is not injective, then the transcendence degree trdeg R A equals 0.

Русский

Если отображение algebraMap R A не инъективно, то трeндентная степень trdeg R A равна 0.

LaTeX

$$$\\\\lnot\\\\ Injective(\\\\text{algebraMap } R A) \\\\Rightarrow \\\\mathrm{trdeg}(R,A) = 0$$$

Lean4

theorem trdeg_eq_zero_of_not_injective (h : ¬Injective (algebraMap R A)) : trdeg R A = 0 :=
  by
  have := isEmpty_algebraicIndependent h
  rw [trdeg, ciSup_of_empty, bot_eq_zero]

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