Mathlib Changelog
v4
Changelog
About
Github
Def
Mathlib.Tactic.addRelatedDecl
Modification history
2023-03-16 04:49
Mathlib/Util/AddRelatedDecl.lean
feat: port `@[elementwise]` attribute (#2882) …
Added
Mathlib.Tactic.addRelatedDecl
View on Github →