aeval_algebraMap_eq_zero_iff_of_injective

English

If the algebra map A→B is injective, then aeval (algebraMap A B x) p = 0 iff aeval x p = 0 for all x ∈ A and p ∈ R[X].

Русский

Если алгебра карта A→B инъективна, то равенство aeval(algebraMap_A_B x) p = 0 эквивалентно aeval x p = 0 для всех x и p.

LaTeX

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

Lean4

theorem aeval_algebraMap_eq_zero_iff_of_injective {x : A} {p : R[X]} (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]

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