aeval_algebraMap_eq_zero_iff_of_injective

English

If the algebra map is injective, then aeval (algebraMap A B ∘ x) p = 0 iff aeval x p = 0.

Русский

Если отображение алгебра является инъективным, то aeval(algebraMap A B ∘ x) p = 0 тогда и только тогда aeval x p = 0.

LaTeX

$$$\operatorname{Injective}(\operatorname{algebraMap} A B) \Longrightarrow (\operatorname{aeval} (\operatorname{algebraMap} A B \circ x) p = 0 \iff \operatorname{aeval} x p = 0)$$$

Lean4

theorem aeval_algebraMap_eq_zero_iff_of_injective {x : σ → A} {p : MvPolynomial σ R}
    (h : Function.Injective (algebraMap A B)) : aeval (algebraMap A B ∘ x) p = 0 ↔ aeval x p = 0 := by
  rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]

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