148structure GenerationPhases where 149 gen1_phase : ℝ := 0
proof body
Definition body.
150 gen2_phase : ℝ := Real.pi / 2 151 gen3_phase : ℝ := Real.pi / 4 152 153/-- The mixing angle between generations is related to their phase difference. -/
depends on (6)
Lean names referenced from this declaration's body.