`BookProof.ChapterF1.bargmann_creat_annih` (m n : ℕ) : bargmann (creat (X ^ m)) (X ^ n) = bargmann (X ^ m) (annih (X ^ n))

Initializing...

`BookProof.ChapterF1.bargmann_creat_annih` (m n : ℕ) : bargmann (creat (X ^ m)) (X ^ n) = bargmann (X ^ m) (annih (X ^ n)) · Prove2Me