map_ne_zero_of_eq_mul — Mathlib

English

If g is distinguished at I and f = g*h, and h ≠ 0 in quotient, then f.map ≠ 0.

Русский

Если g распределён относительно I и f=g*h, и h не нулёво в фактор-кольце, тогда f отображается не нулём.

LaTeX

$$$f,h,g,I\\; (distinguish:g.IsDistinguishedAt I) \\to (notMem: h ≠ 0) \\to (f=g*h) \\to f.map (Ideal.Quotient.mk I) ≠ 0$$$

Lean4

theorem map_ne_zero_of_eq_mul (distinguish : g.IsDistinguishedAt I) (notMem : PowerSeries.constantCoeff h ∉ I)
    (eq : f = g * h) : f.map (Ideal.Quotient.mk I) ≠ 0 := fun H ↦
  by
  have mapf : f.map (Ideal.Quotient.mk I) = (Polynomial.X ^ g.natDegree : (R ⧸ I)[X]) * h.map (Ideal.Quotient.mk I) :=
    by simp [← map_eq_X_pow distinguish, eq]
  apply_fun PowerSeries.coeff g.natDegree at H
  simp [mapf, PowerSeries.coeff_X_pow_mul', eq_zero_iff_mem, notMem] at H

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