repr_ker — Mathlib

English

Equivalence between lifted trdeg under isomorphism of R-algebras.

Русский

Эквивалентность поднятой трансцендентной степени при изоморфизма над R.

LaTeX

$$$\lift(\trdeg R A) = \lift(\trdeg R A').$$$

Lean4

theorem repr_ker (hx : AlgebraicIndependent R x) :
    RingHom.ker (hx.repr : adjoin R (range x) →+* MvPolynomial ι R) = ⊥ :=
  (RingHom.injective_iff_ker_eq_bot _).1
    (AlgEquiv.injective _)
      -- TODO - make this an `AlgEquiv`

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