mathlib3
28b66e1a - doc(tactic/congr): add relationship to `move_add` in `ac_change` (#14618)

Commit
3 years ago
doc(tactic/congr): add relationship to `move_add` in `ac_change` (#14618) This follows #13483, where `move_add` is defined. A big reason for splitting these few lines off the main PR is that they are not in a leaf of the import hierarchy: this hopefully saves lots of CI time, when doing trivial changes to the main PR. This PR should be merged, if #13483 gets merged: they come in a package! Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com>
Author
Parents
Loading