algebraicIndependent_empty_type_iff

English

If ι is empty, AlgebraicIndependent R x holds if and only if the algebra map algebraMap R A is injective.

Русский

Если множество индексов пусто, то AlgebraicIndependent R x эквивалентно инъективности алгебраического отображения algebraMap R A.

LaTeX

$$$[IsEmpty ι] \\Rightarrow \\ AlgebraicIndependent R x \\iff Injective (algebraMap R A)$$$

Lean4

@[simp]
theorem algebraicIndependent_empty_type_iff [IsEmpty ι] : AlgebraicIndependent R x ↔ Injective (algebraMap R A) := by
  rw [algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_injective_iff_of_isEmpty]

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