leadingCoeff_single — Mathlib

English

For a nonempty A and injective D, the leading coefficient of the single basis element (a, r) in R[A] equals r.

Русский

Пусть A непусто, D инъективна; ведущий коэффициент одночлена на позиции a равен r.

LaTeX

$$$(single\ a\ r).leadingCoeff D = r$$$

Lean4

@[simp]
theorem leadingCoeff_single [Nonempty A] (hD : D.Injective) (a : A) (r : R) : (single a r).leadingCoeff D = r := by
  classical
  rw [leadingCoeff, supDegree_single]
  split_ifs with hr
  · simp [hr]
  · rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]

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