Mathlib v3 is deprecated. Go to Mathlib v4

Def short_name1

Modification history

2021-05-26 08:25
test/simps.lean
feat(tactic/simps): implement prefix names (#7596) …
Deleted short_name1View on Github →
2020-07-24 21:19
test/simps.lean
feat(tactic/simps): improvements (#3477) …
Modified short_name1View on Github →
2019-11-04 15:02
test/simps.lean
feat(simps): allow the user to specify the projections (#1630) …
Added short_name1View on Github →