Def a_one_iff_b_one

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 a_one_iff_b_oneView on Github →