Commit 2022-08-19 03:19 33f4d61e

View on Github →

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.

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_hom.coe_prod

added theorem alg_hom.fst_prod

added def alg_hom.prod

added def alg_hom.prod_equiv

added theorem alg_hom.prod_fst_snd

added theorem alg_hom.snd_prod