Def Mathlib.Tactic.Polyrith.Poly.sumM

Modification history

2024-07-15 21:28

Mathlib/Tactic/Polyrith.lean

chore(Tactic): reduce use of autoImplicit, part 3 (#14770)

Modified Mathlib.Tactic.Polyrith.Poly.sumM View on Github →

2022-12-20 23:45

Mathlib/Tactic/Polyrith.lean

feat: `polyrith` tactic (#942) …

Added Mathlib.Tactic.Polyrith.Poly.sumM View on Github →