mathlib3
c781c0ea - feat(data/prod/basic): Involutivity of `prod.map` (#14845)

Commit
3 years ago
feat(data/prod/basic): Involutivity of `prod.map` (#14845) If `f` and `g` are involutive, then so is `prod.map f g`.
Author
Parents
Loading