leadingCoeffHom — Mathlib

English

The map leadingCoeff can be organized as a monoid hom from R[X] to R, i.e., lc(p q) = lc(p) lc(q) and lc(1) = 1, assuming NoZeroDivisors on R.

Русский

Можно рассматривать операцию ведущего коэффициента как гомоморф моноида: lc(p q) = lc(p) lc(q) и lc(1) = 1 при условии, что в R нет нулевых делителей.

LaTeX

$$$\\text{leadingCoeffHom}: R[X] \\to^* R\\quad\\text{with}\\quad \\text{toFun}=\\text{leadingCoeff},\\; \\text{map_one'}=1,\\; \\text{map_mul'}=\\text{leadingCoeff\_mul}.$$$

Lean4

/-- `Polynomial.leadingCoeff` bundled as a `MonoidHom` when `R` has `NoZeroDivisors`, and thus
  `leadingCoeff` is multiplicative -/
def leadingCoeffHom : R[X] →* R where
  toFun := leadingCoeff
  map_one' := by simp
  map_mul' := leadingCoeff_mul

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