Commit 2026-05-10 01:42 15ac5336

View on Github →

fix: rename Pi.prod to Function.prod (#38963) Renames Pi.prod to Function.prod in order to allow for dot notation to work in the non-dependent case.

Estimated changes

modified theorem NonUnitalAlgHom.coe_prod
modified theorem AlgHom.coe_prod
modified theorem MonoidHom.coe_prod
modified theorem MulHom.coe_prod
modified theorem LieHom.coe_prod
deleted theorem Pi.prod_fst_snd
deleted theorem Pi.prod_snd_fst
modified theorem StarAlgHom.coe_prod
modified theorem AffineMap.coe_prod
modified theorem LinearMap.coe_prod
added theorem Function.prod_apply
added theorem Function.prod_fst_snd
added theorem Function.prod_snd_fst