feat: add a simp attribute to isUnit_iff_ne_zero (#11756)

leanprover-community · Mar 29, 2024 · 575260d · 575260d
1 parent 1c32311
commit 575260d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/Mathlib/Algebra/Algebra/Quasispectrum.lean b/Mathlib/Algebra/Algebra/Quasispectrum.lean
@@ -279,7 +279,7 @@ lemma quasispectrum_eq_spectrum_union_zero (R : Type*) {A : Type*} [Semifield R]
     [Algebra R A] (a : A) : quasispectrum R a = spectrum R a ∪ {0} := by
   convert quasispectrum_eq_spectrum_union R a
   ext x
-  simpa using isUnit_iff_ne_zero |>.symm |> not_iff_not.mpr
+  simp
 
 namespace Unitization
 

diff --git a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean
@@ -249,6 +249,7 @@ theorem IsUnit.mk0 (x : G₀) (hx : x ≠ 0) : IsUnit x :=
   (Units.mk0 x hx).isUnit
 #align is_unit.mk0 IsUnit.mk0
 
+@[simp]
 theorem isUnit_iff_ne_zero : IsUnit a ↔ a ≠ 0 :=
   Units.exists_iff_ne_zero
 #align is_unit_iff_ne_zero isUnit_iff_ne_zero