disjoint_ker_aeval_of_isCoprime — Mathlib

English

Under IsCoprime, the join of kernels of aeval f p and aeval f q is contained in the kernel of aeval f (p q).

Русский

При IsCoprime, объединение ядров aeval f p и aeval f q содержится в ядре aeval f (p q).

LaTeX

$$ker(aeval f p) ⊔ ker(aeval f q) ≤ ker(aeval f (p q))$$

Lean4

theorem disjoint_ker_aeval_of_isCoprime (f : M →ₗ[R] M) {p q : R[X]} (hpq : IsCoprime p q) :
    Disjoint (LinearMap.ker (aeval f p)) (LinearMap.ker (aeval f q)) :=
  by
  rw [disjoint_iff_inf_le]
  intro v hv
  rcases hpq with ⟨p', q', hpq'⟩
  simpa [LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).1, LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).2] using
    congr_arg (fun p : R[X] => aeval f p v) hpq'.symm

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