degree_map_lt — Mathlib

English

Let f be a ring homomorphism and p ≠ 0 with f(p.leadingCoeff) = 0. Then the degree of p.map f is strictly less than the degree of p: degree(p.map f) < degree(p).

Русский

Пусть f — кольцо-гомоморфизм и p ≠ 0; если f(p.leadingCoeff) = 0, то deg(p.map f) < deg(p).

LaTeX

$$$\\deg(p.map\\ f) < \\deg(p)$$$

Lean4

theorem degree_map_lt (hp : f p.leadingCoeff = 0) (hp₀ : p ≠ 0) : (p.map f).degree < p.degree :=
  by
  refine degree_map_le.lt_of_ne fun hpq ↦ hp₀ ?_
  rw [leadingCoeff, ← coeff_map, ← natDegree_eq_natDegree hpq, ← leadingCoeff, leadingCoeff_eq_zero] at hp
  rw [← degree_eq_bot, ← hpq, hp, degree_zero]

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