Maintainer merge (comment)

[Merged by Bors] - chore: move `mul_ite`, add `dite` version, multiplicativise `ite_add_ite` #66068

Sign in to view logs

Triggered via issue October 20, 2024 22:26

mathlib-bors[bot]

commented on #17963 69bbcb4

Status Skipped

Total duration 2s

Artifacts –

maintainer_merge_comment.yml

on: issue_comment

Ping maintainers on Zulip