Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-02-15 04:55
f52a0950
View on Github →
feat port/CategoryTheory.Pi.Basic (
#2230
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Pi/Basic.lean
added
theorem
CategoryTheory.Functor.eqToHom_proj
added
def
CategoryTheory.Functor.pi'
added
theorem
CategoryTheory.Functor.pi'_eval
added
def
CategoryTheory.Functor.pi
added
theorem
CategoryTheory.Functor.pi_ext
added
def
CategoryTheory.NatTrans.pi
added
def
CategoryTheory.Pi.comap
added
def
CategoryTheory.Pi.comapComp
added
def
CategoryTheory.Pi.comapEvalIsoEval
added
def
CategoryTheory.Pi.comapId
added
theorem
CategoryTheory.Pi.comp_apply
added
def
CategoryTheory.Pi.eval
added
theorem
CategoryTheory.Pi.id_apply
added
def
CategoryTheory.Pi.isoApp
added
theorem
CategoryTheory.Pi.isoApp_refl
added
theorem
CategoryTheory.Pi.isoApp_symm
added
theorem
CategoryTheory.Pi.isoApp_trans
added
def
CategoryTheory.Pi.sum