Commit 2021-03-24 16:04 b4373e5a

View on Github →

feat(tactic/lint): linter for @[class] def (#6061) Also cleaning up some uses of @[class] def that were missed in #6028.

Estimated changes

modified theorem fact.elim
deleted def fact
added theorem fact_iff
modified theorem T.zero_lt_one
modified theorem abs_nonneg'