Mathlib v3 is deprecated. Go to Mathlib v4

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_one View on Github →