Physlib.Relativity.Fermions.Weyl.DualRightHanded

The equivalence `Fermion.DualRightHandedWeyl.toFin2ℂFun` defines an isomorphism between the space of dual right-handed Weyl fermions and the complex vector space $\mathbb{C}^2$, represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$. This identifies the specific fermion structure with its underlying coordinate representation.

The space of dual right-handed Weyl fermions, which is defined as a wrapper around $\mathbb{C}^2$, is equipped with the structure of an additive commutative monoid. This means that for any two dual right-handed Weyl fermions, there is a well-defined addition operation that is associative and commutative, and there exists a zero element that acts as the additive identity.

The space of dual right-handed Weyl fermions is equipped with the structure of an additive commutative group. This defines the operations of addition, negation, and the zero element for these spinors, corresponding to the standard vector space operations on $\mathbb{C}^2$.