Commit 2023-04-18 03:37 68044747

View on Github →

feat: port Control.Bitraversable.Lemmas (#3460)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/Bitraversable/Lemmas.lean

added theorem Bitraversable.comp_tfst

added theorem Bitraversable.comp_tsnd

added theorem Bitraversable.id_tfst

added theorem Bitraversable.id_tsnd

added def Bitraversable.tfst

added theorem Bitraversable.tfst_eq_fst_id

added theorem Bitraversable.tfst_tsnd

added def Bitraversable.tsnd

added theorem Bitraversable.tsnd_eq_snd_id

added theorem Bitraversable.tsnd_tfst