Mathlib v3 is deprecated. Go to Mathlib v4

Theorem spectrum.one_eq

Modification history

2021-12-09 16:26

src/algebra/algebra/spectrum.lean

feat(algebra/algebra/spectrum): lemmas when scalars are a field (#10476) …

Added spectrum.one_eq View on Github →