lint and suggest

[Merged by Bors] - chore: rename `StructureGroupoid.eq_on_source'` to `StructureGroupoid.mem_of_eqOnSource'` #15343

Sign in to view logs

Triggered via pull request January 19, 2024 06:47

winstonyin

synchronize #9802

wy_EqOnSource

Status Success

Total duration 50s

Artifacts –

lint_and_suggest_pr.yml

on: pull_request

Check all files imported