intCast_inj — Mathlib

English

Let m,n ∈ ℤ and R be a ring of characteristic zero. The constant polynomials m and n in R[X] are equal if and only if m = n.

Русский

Пусть m,n ∈ ℤ и R — кольцо характеристик 0. Константные полиномы m и n в R[X] равны тогда и только тогда, когда m = n.

LaTeX

$$$ (m : R[X]) = (n : R[X]) \\iff m = n $$$

Lean4

@[norm_cast]
theorem intCast_inj {m n : ℤ} {R : Type*} [Ring R] [CharZero R] : (↑m : R[X]) = ↑n ↔ m = n :=
  by
  constructor
  · intro h
    apply_fun fun p => p.coeff 0 at h
    simpa using h
  · rintro rfl
    rfl

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