injective — Mathlib

English

Let f: A → A' be an algebra homomorphism. If f is injective, then AlgebraicIndependent R (f ∘ x) is equivalent to AlgebraicIndependent R x.

Русский

Пусть f: A → A' — алгебраический гомоморфизм и инъективен. Тогда AlgebraicIndependent R (f ∘ x) эквивалентно AlgebraicIndependent R x.

LaTeX

$$$\\\\mathrm{AlgHom}\\\\(R,A,A') \\\\text{ with injective } f \\\\Rightarrow \\\\mathrm{AlgebraicIndependent}(R,(f\\\\circ x)) \\\\iff \\\\mathrm{AlgebraicIndependent}(R,x)$$$

Lean4

protected theorem injective [Nontrivial R] : Injective x :=
  hx.linearIndependent.injective

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