aeval_ne_zero_of_isCoprime — Mathlib

English

Let p, q ∈ R[X] be coprime. Then for every s in S, either aeval_s(p) ≠ 0 or aeval_s(q) ≠ 0.

Русский

Пусть p, q ∈ R[X] неприводимы между собой. Тогда для каждого s ∈ S хотя бы одно из значений aeval_s(p), aeval_s(q) не равно нулю.

LaTeX

$$$\text{IsCoprime}(p,q) \Rightarrow \forall s \in S,\; aeval_s(p) \neq 0 \;\text{or}\; aeval_s(q) \neq 0.$$$

Lean4

theorem aeval_ne_zero_of_isCoprime {R} [CommSemiring R] [Nontrivial S] [Semiring S] [Algebra R S] {p q : R[X]}
    (h : IsCoprime p q) (s : S) : aeval s p ≠ 0 ∨ aeval s q ≠ 0 :=
  by
  by_contra! hpq
  rcases h with ⟨_, _, h⟩
  apply_fun aeval s at h
  simp only [map_add, map_mul, map_one, hpq.left, hpq.right, mul_zero, add_zero, zero_ne_one] at h

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