isRegular — Mathlib

English

If p is monic, then p is regular in R[X], i.e., left and right cancellation by p holds.

Русский

Если p мононичен, то p является регулярным в R[X], то есть слева и справа выполняются тождественные сокращения.

LaTeX

$$$\forall {R} [\text{Ring } R] {p : Polynomial R}, p.Monic \rightarrow IsRegular p$$$

Lean4

theorem isRegular {R : Type*} [Ring R] {p : R[X]} (hp : Monic p) : IsRegular p :=
  by
  constructor
  · intro q r h
    dsimp only at h
    rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
  · intro q r h
    simp only at h
    rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]

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