eq_one_of_map_eq_one — Mathlib

English

Let f be a ring homomorphism, p monic, and p.map f = 1. Then p = 1.

Русский

Пусть f — гомоморфизм колец, p моноическое, и p.map f = 1. Тогда p = 1.

LaTeX

$$$\text{Monic}(p) \land p \mapsto 1 \Rightarrow p = 1$$$

Lean4

theorem eq_one_of_map_eq_one {S : Type*} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : p.Monic)
    (map_eq : p.map f = 1) : p = 1 := by
  nontriviality R
  have hdeg : p.degree = 0 :=
    by
    rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]
    · rw [hp.leadingCoeff, f.map_one]
      exact one_ne_zero
  have hndeg : p.natDegree = 0 := WithBot.coe_eq_coe.mp ((degree_eq_natDegree hp.ne_zero).symm.trans hdeg)
  convert eq_C_of_degree_eq_zero hdeg
  rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]

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