Inductive Mathlib.Tactic.Ring.ExceptType

Modification history

2024-10-08 07:22
Mathlib/Tactic/Ring/Compare.lean
feat: `ring`-based prover for certain inequalities in semirings (#16840) …
Added Mathlib.Tactic.Ring.ExceptTypeView on Github →