Prove2Me

`BookProof.WeylHamiltonian.weylHamiltonian_isSelfAdjoint` {n m : ℕ} (π : Fin n → H →L[ℂ] H) (B : Fin m → H →L[ℂ] H) (hπ : ∀ i, IsSelfAdjoint (π i)) (hB : ∀ a, IsSelfAdjoint (B a))

Proved
BookProof.WeylHamiltonian.weylHamiltonian_isSelfAdjoint

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterWeylHamiltonian.

BookProof.WeylHamiltonian.weylHamiltonian_isSelfAdjoint {n m : ℕ} (π : Fin n → H →L[ℂ] H) (B : Fin m → H →L[ℂ] H) (hπ : ∀ i, IsSelfAdjoint (π i)) (hB : ∀ a, IsSelfAdjoint (B a)) : IsSelfAdjoint (weylHamiltonian π B)

Formalization note: Lean 4 identifier BookProof.WeylHamiltonian.weylHamiltonian_isSelfAdjoint.

Preamble
-- Generated from ChapterWeylHamiltonian.lean — theorem BookProof.WeylHamiltonian.weylHamiltonian_isSelfAdjoint
import Mathlib
import Definitions.Def_ChapterWeylHamiltonian
open BookProof.WeylHamiltonian



open ContinuousLinearMap
open scoped BigOperators

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
Formal statement
theorem BookProof.WeylHamiltonian.weylHamiltonian_isSelfAdjoint {n m : ℕ}
    (π : Fin n → H →L[ℂ] H) (B : Fin m → H →L[ℂ] H)
    (hπ : ∀ i, IsSelfAdjoint (π i)) (hB : ∀ a, IsSelfAdjoint (B a)) :
    IsSelfAdjoint (weylHamiltonian π B) := by sorry

View graph