[Merged by Bors] - chore(Order/CompleteSublattice): correct the argument type of subtype_apply
#39150
Triggered via pull request
September 7, 2026 13:43
mathlib-bors[bot]
edited
#43527
Status
Skipped
Total duration
1s
Artifacts
–