leadingCoeff

Mathlib.Algebra.MonoidAlgebra.Degree

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.leadingCoeff

Lean4

/-- If `D` is an injection into a linear order `B`, the leading coefficient of `f : R[A]` is the
  nonzero coefficient of highest degree according to `D`, or 0 if `f = 0`. In general, it is defined
  to be the coefficient at an inverse image of `supDegree f` (if such exists). -/
noncomputable def leadingCoeff [Nonempty A] (f : R[A]) : R :=
  f (D.invFun <| f.supDegree D)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru