`BookProof.ChapterGaugeUnconstrainedSpectrum.diagOp_injective` : Function.Injective (diagOp (X := X))

Proved

BookProof.ChapterGaugeUnconstrainedSpectrum.diagOp_injective

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGaugeUnconstrainedSpectrum.

BookProof.ChapterGaugeUnconstrainedSpectrum.diagOp_injective : Function.Injective (diagOp (X := X))

Formalization note: Lean 4 identifier BookProof.ChapterGaugeUnconstrainedSpectrum.diagOp_injective.

Preamble

-- Generated from ChapterGaugeUnconstrainedSpectrum.lean — theorem BookProof.ChapterGaugeUnconstrainedSpectrum.diagOp_injective
import Mathlib
import Definitions.Def_ChapterGaugeUnconstrainedSpectrum
import Definitions.Def_ChapterAbelianDiagonalCountable
open BookProof.ChapterAbelianDiagonalCountable
open BookProof.ChapterGaugeUnconstrainedSpectrum



variable {X : Type*}

Formal statement

theorem BookProof.ChapterGaugeUnconstrainedSpectrum.diagOp_injective : Function.Injective (diagOp (X := X)) := by sorry

View graph