Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-20 17:11
a5db36af
View on Github →
Feat: Port data.prod.tprod (
#1464
) Port of data.prod.tprod
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/Prod/TProd.lean
added
theorem
List.TProd.elim_mk
added
theorem
List.TProd.elim_of_mem
added
theorem
List.TProd.elim_of_ne
added
theorem
List.TProd.elim_self
added
theorem
List.TProd.ext
added
theorem
List.TProd.fst_mk
added
theorem
List.TProd.mk_elim
added
def
List.TProd.piEquivTProd
added
theorem
List.TProd.snd_mk
added
def
List.TProd
added
theorem
Set.elim_preimage_pi
added
theorem
Set.mk_preimage_tprod