mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore(Algebra.Ring.InjSurj): remove redundant `mul` and `add` fields

Open mattrobball opened this issue 1 year ago • 1 comments

Lean can figure these out and if inferred instance of Mul (or Add) contains non-reducible terms, it will block unification.

  • [ ] depends on: #11521

Open in Gitpod

mattrobball avatar Mar 24 '24 18:03 mattrobball

This PR/issue depends on:

leanprover-community-mathlib4-bot avatar Mar 25 '24 02:03 leanprover-community-mathlib4-bot