term_⟮_,,⟯

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

URI: https://scilib.ai/kg/mathlib#IntermediateField.term_⟮_,,⟯

Lean4

/-- If `x₁ x₂ ... xₙ : E` then `F⟮x₁,x₂,...,xₙ⟯` is the `IntermediateField F E`
generated by these elements. -/
@[scoped term_parser 1000]
public meta def «term_⟮_,,⟯» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `IntermediateField.«term_⟮_,,⟯» 1024 0
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "⟮")
        ((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
          Bool.false✝))
      (ParserDescr.symbol✝ "⟯"))

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

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

Разделы

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

Аффилиация

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