Theorem Units.zero_not_mem_spectrum

Modification history

2025-05-25 12:30

Mathlib/Algebra/Algebra/Spectrum/Basic.lean

chore(*): not_mem/nmem -> notMem (#25159)

Deleted Units.zero_not_mem_spectrum View on Github →

2024-08-31 20:17

Mathlib/Algebra/Algebra/Spectrum.lean

feat: add a `simp` lemma: `Units.zero_not_mem_spectrum` (#16339)

Added Units.zero_not_mem_spectrum View on Github →