Mathlib v3 is deprecated. Go to Mathlib v4

Def no_to_additive

Modification history

2022-05-04 17:58
test/lint_to_additive_doc.lean
fix(src/tactic/alias): Teach `get_alias_target` about `alias f ↔ a b` (#13742) …
Deleted no_to_additiveView on Github →
2022-03-19 17:43
test/lint_to_additive_doc.lean
chore(*): update to lean 3.42.0c (#12818)
Added no_to_additiveView on Github →