mathlib3
33f4d61e - feat(algebra/algebra/basic):add `alg_hom.prod` (#16116)

Commit
3 years ago
feat(algebra/algebra/basic):add `alg_hom.prod` (#16116) This adds `alg_hom.prod` to go with `alg_hom.fst` and `alg_hom.snd`. It was noticed to be missing during #16089.
Author
Parents
Loading