From b251161701a41d8019e9d5c5030695047cf311f6 Mon Sep 17 00:00:00 2001
From: Peiran Wu <15968905+wupr@users.noreply.github.com>
Date: Mon, 24 Jun 2024 17:14:56 +0100
Subject: [PATCH] Add two lemmas

---
 Mathlib/Algebra/Group/TypeTags.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Mathlib/Algebra/Group/TypeTags.lean b/Mathlib/Algebra/Group/TypeTags.lean
index bbea749a4e42c5..3ba30064df532d 100644
--- a/Mathlib/Algebra/Group/TypeTags.lean
+++ b/Mathlib/Algebra/Group/TypeTags.lean
@@ -249,6 +249,11 @@ theorem ofMul_eq_zero {A : Type*} [One A] {x : A} : Additive.ofMul x = 0 ↔ x =
 theorem toMul_zero [One α] : toMul (0 : Additive α) = 1 := rfl
 #align to_mul_zero toMul_zero
 
+@[simp]
+lemma toMul_eq_one {α : Type*} [One α] {x : Additive α} :
+    Additive.toMul x = 1 ↔ x = 0 :=
+  Iff.rfl
+
 instance [Zero α] : One (Multiplicative α) :=
   ⟨Multiplicative.ofAdd 0⟩
 
@@ -267,6 +272,11 @@ theorem toAdd_one [Zero α] : toAdd (1 : Multiplicative α) = 0 :=
   rfl
 #align to_add_one toAdd_one
 
+@[simp]
+lemma toAdd_eq_zero {α : Type*} [Zero α] {x : Multiplicative α} :
+    Multiplicative.toAdd x = 0 ↔ x = 1 :=
+  Iff.rfl
+
 instance Additive.addZeroClass [MulOneClass α] : AddZeroClass (Additive α) where
   zero := 0
   add := (· + ·)