term__[_⁻¹_] — Mathlib

English

The fraction r / s maps to a formal fraction in the Ore localization, and equality respects representatives.

Русский

Дробь r / s отображается в Ore локализацию, равенство сохраняется при замене представителя.

LaTeX

$$$\forall r\in X, s\in S:\; r / s \in X[S^{-1}]$$$

Lean4

@[inherit_doc OreLocalization, scoped term_parser 1000]
public meta def «term__[_⁻¹_]» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `OreLocalization.«term__[_⁻¹_]» 1075 0
    (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `noWs)
      (ParserDescr.unary✝ `atomic
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "[") (ParserDescr.cat✝ `term 0))
              (ParserDescr.symbol✝ "⁻¹"))
            (ParserDescr.const✝ `noWs))
          (ParserDescr.symbol✝ "]"))))

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