[Merged by Bors] - chore: standardise names for coercions from morphism classes to morphisms #39144
Triggered via pull request
September 7, 2026 13:23
mathlib-bors[bot]
mathlib-bors[bot]
edited
#43367
Status
Skipped
Total duration
11s
Artifacts
–
check_pr_titles.yaml
on: pull_request_target
check_title
0s