Commit 2023-11-03 09:34 8b4ab5e7
View on Github →chore: rename eq_of_eq_on_source_univ to eq_of_eqOnSource_univ (#8121) Matches the naming convention, zulip discussion. This is probably a left-over from the port; in mathlib3, the hypothesis and the lemma were named using "eq_on_source". In passing, we also
- add missing periods to all docstrings involved
- add a docstring for the LocalHomeomorph version (matching its LocalEquiv clone)
- fix a missed rename in a doc comment.