`BookProof.ChapterG2.brst_physical_iff_gauge_invariant` (a : A) : (![a, 0] ∈ brstKer Q) ↔ Q * a = 0
ProvedBookProof.ChapterG2.brst_physical_iff_gauge_invarianttheoremstimepiece
Prove the following Lean 4 theorem from ChapterG2.
BookProof.ChapterG2.brst_physical_iff_gauge_invariant (a : A) : (![a, 0] ∈ brstKer Q) ↔ Q * a = 0
Formalization note: Lean 4 identifier BookProof.ChapterG2.brst_physical_iff_gauge_invariant.
Preamble
-- Generated from ChapterG2.lean — theorem BookProof.ChapterG2.brst_physical_iff_gauge_invariant
import Mathlib
import Definitions.Def_ChapterG2
open BookProof.ChapterG2
open MeasureTheory ProbabilityTheory
open scoped ProbabilityTheory
variable {Ω : Type*} [MeasurableSpace Ω]
variable {A : Type*} [CommRing A] (Q : A)Formal statement
theorem BookProof.ChapterG2.brst_physical_iff_gauge_invariant (a : A) :
(![a, 0] ∈ brstKer Q) ↔ Q * a = 0 := by sorry