Commit 2026-07-01 01:31 79841fc9

View on Github →

feat: expand lemmas about Function.prod (#41148)

Estimated changes

Modified Mathlib/Logic/Function/Defs.lean

added theorem Function.const_prod

added theorem Function.fst_comp_prod

added theorem Function.map_comp_prod

modified theorem Function.prod_apply

added theorem Function.prod_comp

added theorem Function.prod_comp_fst_comp_snd

added theorem Function.prod_comp_prod

added theorem Function.prod_const_const

added theorem Function.prod_def

added theorem Function.prod_ext_iff

added theorem Function.prod_fst_comp_snd_comp

modified theorem Function.prod_fst_snd

added theorem Function.prod_inj

modified theorem Function.prod_snd_fst

added theorem Function.snd_comp_prod

added theorem Function.swap_comp_prod