diff --git a/HepLean/PerturbationTheory/FieldStruct/Basic.lean b/HepLean/PerturbationTheory/FieldStruct/Basic.lean index 9d76c563..8b7feab0 100644 --- a/HepLean/PerturbationTheory/FieldStruct/Basic.lean +++ b/HepLean/PerturbationTheory/FieldStruct/Basic.lean @@ -19,7 +19,7 @@ structure FieldStruct where /-- The type of fields. This also includes anti-states. -/ Fields : Type /-- The specification if a field is bosonic or fermionic. -/ - statistics : 𝓕 → FieldStatistic + statistics : Fields → FieldStatistic namespace FieldStruct variable (𝓕 : FieldStruct)