Mathlib v3 is deprecated. Go to Mathlib v4

Def without_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) …
Added without_to_additiveView on Github →