aeval_algebraMap_eq_zero_iff — Mathlib

English

If NoZeroSMulDivisors of A into B and B is nontrivial, then aeval (algebraMap A B ∘ x) p = 0 iff aeval x p = 0.

Русский

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

LaTeX

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

Lean4

theorem aeval_algebraMap_eq_zero_iff [NoZeroSMulDivisors A B] [Nontrivial B] (x : σ → A) (p : MvPolynomial σ R) :
    aeval (algebraMap A B ∘ x) p = 0 ↔ aeval x p = 0 := by
  rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero, iff_false_intro (one_ne_zero' B), or_false]

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