Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-27 18:48 786c7375

View on Github →

feat(logic/basic): trivial transport lemmas (#2254)

feat(logic/basic): trivial transport lemmas
oops

Estimated changes

Modified src/category_theory/limits/shapes/equalizers.lean

Modified src/data/nat/basic.lean

Modified src/logic/basic.lean

added theorem eq_mp_rfl

added theorem eq_mpr_rfl

added theorem eq_rec_constant