mathlib3
[Merged by Bors] - feat(*/prod): `prod_prod_prod` equivs
#19235

Closed

[Merged by Bors] - feat(*/prod): `prod_prod_prod` equivs #19235

eric-wieser wants to merge 6 commits into master from eric-wieser/prod-commutative

feat(*/prod): `prod_prod_prod` equivs

0d275081

tweak

81401448

eric-wieser added awaiting-review

eric-wieser added t-algebra

github-actions added modifies-synchronized-file

Update prod.lean

7b5752c6

Update prod.lean

ee7f760f

@fix@

b5929923

github-actions added delegated

github-actions removed awaiting-review

docstring

2ca4d42a

github-actions added ready-to-merge

bors changed the title ~~feat(*/prod): `prod_prod_prod` equivs~~ [Merged by Bors] - feat(*/prod): `prod_prod_prod` equivs 2 years ago

bors closed this 2 years ago

bors deleted the eric-wieser/prod-commutative branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge delegated t-algebra modifies-synchronized-file

Milestone

No milestone