monicityMacro

Mathlib.Tactic.ComputeDegree

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.ComputeDegree.monicityMacro

Lean4

/-- `monicity` tries to solve a goal of the form `Monic f`.
It converts the goal into a goal of the form `natDegree f ≤ n` and one of the form `f.coeff n = 1`
and calls `compute_degree` on those two goals.

The variant `monicity!` starts like `monicity`, but calls `compute_degree!` on the two side-goals.
-/
@[tactic_parser 1000]
public meta def monicityMacro : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.ComputeDegree.monicityMacro 1024 (ParserDescr.nonReservedSymbol✝ "monicity" false✝)

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

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

Разделы

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

Аффилиация

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