Commit 2022-11-07 04:25 b902a2ae

View on Github →

feat: port Data.Prod.Basic (#545) moves and restructures existing Data.Prod

Estimated changes

deleted theorem Prod.eq_iff_fst_eq_snd_eq
deleted theorem Prod.exists'
deleted theorem Prod.ext'
deleted theorem Prod.ext_iff
deleted theorem Prod.forall'
deleted theorem Prod.fst_eq_iff
deleted theorem Prod.fst_injective
deleted theorem Prod.fst_surjective
deleted theorem Prod.fst_swap
deleted theorem Prod.id_prod
deleted theorem Prod.lex_def
deleted theorem Prod.map_comp_map
deleted theorem Prod.map_def
deleted theorem Prod.map_fst'
deleted theorem Prod.map_fst
deleted theorem Prod.map_map
deleted theorem Prod.map_mk
deleted theorem Prod.map_snd'
deleted theorem Prod.map_snd
deleted theorem Prod.mk.inj_iff
deleted theorem Prod.mk.inj_left
deleted theorem Prod.mk.inj_right
deleted theorem Prod.snd_eq_iff
deleted theorem Prod.snd_injective
deleted theorem Prod.snd_surjective
deleted theorem Prod.snd_swap
deleted def Prod.swap
deleted theorem Prod.swap_LeftInverse
deleted theorem Prod.swap_RightInverse
deleted theorem Prod.swap_bijective
deleted theorem Prod.swap_inj
deleted theorem Prod.swap_injective
deleted theorem Prod.swap_prod_mk
deleted theorem Prod.swap_surjective
deleted theorem Prod.swap_swap
deleted theorem Prod.swap_swap_eq
deleted theorem Prod.«exists»
deleted theorem Prod.«forall»
deleted theorem prod_map
added theorem Prod.Lex.refl_left
added theorem Prod.Lex.refl_right
added theorem Prod.Lex.trans
added theorem Prod.Lex_def
added theorem Prod.exists'
added theorem Prod.ext'
added theorem Prod.ext_iff
added theorem Prod.forall'
added theorem Prod.fst_comp_mk
added theorem Prod.fst_eq_iff
added theorem Prod.fst_injective
added theorem Prod.fst_surjective
added theorem Prod.fst_swap
added theorem Prod.id_prod
added theorem Prod.map_comp_map
added theorem Prod.map_def
added theorem Prod.map_fst'
added theorem Prod.map_fst
added theorem Prod.map_id
added theorem Prod.map_map
added theorem Prod.map_mk
added theorem Prod.map_snd'
added theorem Prod.map_snd
added theorem Prod.mk.inj_iff
added theorem Prod.mk.inj_left
added theorem Prod.mk.inj_right
added theorem Prod.snd_comp_mk
added theorem Prod.snd_eq_iff
added theorem Prod.snd_injective
added theorem Prod.snd_surjective
added theorem Prod.snd_swap
added def Prod.swap
added theorem Prod.swap_bijective
added theorem Prod.swap_inj
added theorem Prod.swap_injective
added theorem Prod.swap_leftInverse
added theorem Prod.swap_prod_mk
added theorem Prod.swap_rightInverse
added theorem Prod.swap_surjective
added theorem Prod.swap_swap
added theorem Prod.swap_swap_eq
added theorem Prod.«exists»
added theorem Prod.«forall»
added theorem Prod_map