Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-12 02:28 09d0f028

View on Github →

chore({category_theory,order}/category/*): Missing dsimp lemmas (#12593) Add the dsimp lemmas stating ↥(of α) = α . Also rename the few to_dual functors to dual to match the other files.

Estimated changes

added theorem Bipointed.coe_of
added theorem PartialFun.coe_of
added theorem Pointed.coe_of
added theorem Twop.coe_of
added theorem Twop.coe_to_Bipointed
added theorem BoolAlg.coe_of
added theorem BoundedLattice.coe_of
added theorem BoundedOrder.coe_of
added theorem CompleteLattice.coe_of
added theorem DistribLattice.coe_of
added theorem FinPartialOrder.coe_of
added theorem Frame.coe_of
added theorem Lattice.coe_of
added theorem LinearOrder.coe_of
added theorem PartialOrder.coe_of
added theorem Preorder.coe_of
added def Preorder.dual
deleted def Preorder.to_dual
added theorem ωCPO.coe_of