aeval_algebraMap_eq_zero_iff — Mathlib

English

Let no-zero-smul-divisors hold and B be nontrivial. For x ∈ A and p ∈ R[X], aeval (algebraMap A B x) p = 0 iff aeval x p = 0.

Русский

Пусть выполняются условия NoZeroSmulDivisors и B не тривиален. Тогда aeval(algebraMap_A_B x) p = 0 эквивалентно aeval x p = 0.

LaTeX

$$$$\\mathrm{aeval}_{\\mathrm{algebraMap}_{A\\to B} (x)}(p) = 0 \\;\\iff\\; \\mathrm{aeval}_{x}(p) = 0.$$$$

Lean4

@[simp]
theorem aeval_algebraMap_eq_zero_iff [NoZeroSMulDivisors A B] [Nontrivial B] (x : A) (p : R[X]) :
    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]

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