Registry · Proposition IV.P23 tau-effective formalized

IV.P23 — Commutator Equals Lifted Lie Bracket

[X̂, Ŷ] = [X,Y]^: operator commutator equals the operator of the Lie bracket. Bridges geometry and algebra.

Book IV Part 3 Ch. 19

Dependency Graph

Depends on (2)

IV.D65 IV.D66

Depended on by (1)

IV.T21

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.Quantization

Symbol: Tau.BookIV.QuantumMechanics.CommutatorEqualsLiftedLieBracket