chore(data/equiv/mul_add): add missing to_equiv_mk (#9765)

leanprover-community · Oct 17, 2021 · 678d7ed · 678d7ed
1 parent 24ebeec
commit 678d7ed
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/data/equiv/mul_add.lean b/src/data/equiv/mul_add.lean
@@ -143,6 +143,10 @@ theorem to_equiv_symm (f : M ≃* N) : f.symm.to_equiv = f.to_equiv.symm := rfl
 @[simp, to_additive]
 theorem coe_mk (f : M → N) (g h₁ h₂ h₃) : ⇑(mul_equiv.mk f g h₁ h₂ h₃) = f := rfl
 
+@[simp, to_additive]
+lemma to_equiv_mk (f : M → N) (g : N → M) (h₁ h₂ h₃) :
+  (mk f g h₁ h₂ h₃).to_equiv = ⟨f, g, h₁, h₂⟩ := rfl
+
 @[simp, to_additive]
 lemma symm_symm : ∀ (f : M ≃* N), f.symm.symm = f
 | ⟨f, g, h₁, h₂, h₃⟩ := rfl