ring1NF — Mathlib

Lean4
/-- Tactic for solving equations of *commutative* (semi)rings, allowing variables in the exponent.

* This version of `ring1` uses `ring_nf` to simplify in atoms.
* The variant `ring1_nf!` will use a more aggressive reducibility setting
  to determine equality of atoms.
-/
@[tactic_parser 1000]
public meta def ring1NF : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.RingNF.ring1NF 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "ring1_nf" false✝)
        (ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "!")))
      Lean.Parser.Tactic.optConfig)
Похожие утверждения