Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_equiv.mk_coe

Modification history

2021-03-03 07:35

src/data/equiv/ring.lean

chore(data/equiv): add missing simp lemmas about mk (#6505) …

Added ring_equiv.mk_coe View on Github →