Def Mathlib.Tactic.Ring.evalMul₁

Modification history

2024-09-29 03:27

Mathlib/Tactic/Ring/Basic.lean

fix: call checkSystem in `linarith` and `ring` (#16666) …

Modified Mathlib.Tactic.Ring.evalMul₁ View on Github →

2024-07-19 08:06

Mathlib/Tactic/Ring/Basic.lean

chore(Tactic/Ring/Basic): reduce use of autoImplicit (#14709)

Modified Mathlib.Tactic.Ring.evalMul₁ View on Github →

2022-11-07 21:53

Mathlib/Tactic/Ring.lean

feat: `ring_nf` tactic (#552) …

Modified Mathlib.Tactic.Ring.evalMul₁ View on Github →

2022-11-01 23:28

Mathlib/Tactic/Ring.lean

feat: `ring_exp` tactic, subtraction in `ring` (#519) …

Added Mathlib.Tactic.Ring.evalMul₁ View on Github →