monic_mul_C_of_leadingCoeff_mul_eq_one

English

If b ∈ R satisfies p.leadingCoeff · b = 1, then C b · p is monic.

Русский

Пусть b ∈ R и p.leadingCoeff · b = 1; тогда C b · p моничен.

LaTeX

$$$\text{If } b \in R \text{ with } p.leadingCoeff \cdot b = 1,\; (C b \cdot p)\text{ Monic}.$$$

Lean4

theorem monic_mul_C_of_leadingCoeff_mul_eq_one {b : R} (hp : p.leadingCoeff * b = 1) : Monic (p * C b) :=
  by
  unfold Monic
  nontriviality
  rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]

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