theorem MixPi2Lambda.mutation_type10_ne {ε ε' : GeneType} {m n : ℕ} (h_le : m ≤ n) : Gene.ofRank (2 * m + 2) ε + Gene.ofRank (2 * n + 2) ε' ≠ Gene.ofRank (2 * m) ε + Gene.ofRank (2 * n + 4) ε'

theorem MixPi2Lambda.mutation_type10_iterate_signature_eq {ε ε' : GeneType} {m n : ℕ} (h_le : m ≤ n) (i k : ℕ) (hi : i ≤ k) : Chromosome.signature ((⇑Chromosome.prime)^[i] (Gene.ofRank (2 * m + 2 + k) ε + Gene.ofRank (2 * n + 2 + k) ε')) = Chromosome.signature ((⇑Chromosome.prime)^[i] (Gene.ofRank (2 * m + k) ε + Gene.ofRank (2 * n + 4 + k) ε'))

theorem MixPi2Lambda.mutation_type10_signature_eq {ε ε' : GeneType} {m n : ℕ} (h_le : m ≤ n) : Chromosome.signature (Gene.ofRank (2 * m + 2) ε + Gene.ofRank (2 * n + 2) ε') = Chromosome.signature (Gene.ofRank (2 * m) ε + Gene.ofRank (2 * n + 4) ε')

theorem MixPi2Lambda.mutation_type10_le {ε ε' : GeneType} {m n : ℕ} (h_le : m ≤ n) : Gene.ofRank (2 * m + 2) ε + Gene.ofRank (2 * n + 2) ε' ≤ Gene.ofRank (2 * m) ε + Gene.ofRank (2 * n + 4) ε'

noncomputable def MixPi2Lambda.X10 {ε ε' : GeneType} {m n : ℕ} (h_le : m ≤ n) (hε : ε ≠ GeneType.NonPolarized) (hε' : ε' ≠ GeneType.NonPolarized) : ↥(Variety.Mix (Variety.Pi, 2 • Variety.Lambda))

Equations

• MixPi2Lambda.X10 h_le hε hε' = ⟨Gene.ofRank (2 * m + 2) ε + Gene.ofRank (2 * n + 2) ε', ⋯⟩

theorem MixPi2Lambda.X10_eq {ε ε' : GeneType} {m n : ℕ} (h_le : m ≤ n) (hε : ε ≠ GeneType.NonPolarized) (hε' : ε' ≠ GeneType.NonPolarized) : ↑(X10 h_le hε hε') = Gene.ofRank (2 * m + 2) ε + Gene.ofRank (2 * n + 2) ε'

@[simp]

theorem MixPi2Lambda.neg_X10 {ε ε' : GeneType} {m n : ℕ} (h_le : m ≤ n) (hε : ε ≠ GeneType.NonPolarized) (hε' : ε' ≠ GeneType.NonPolarized) : -X10 h_le hε hε' = X10 h_le ⋯ ⋯

noncomputable def MixPi2Lambda.Y10 {ε ε' : GeneType} {m n : ℕ} (h_le : m ≤ n) (hε : ε ≠ GeneType.NonPolarized) (hε' : ε' ≠ GeneType.NonPolarized) : ↥(Variety.Mix (Variety.Pi, 2 • Variety.Lambda))

Equations

• MixPi2Lambda.Y10 h_le hε hε' = ⟨Gene.ofRank (2 * m) ε + Gene.ofRank (2 * n + 4) ε', ⋯⟩

theorem MixPi2Lambda.Y10_eq {ε ε' : GeneType} {m n : ℕ} (h_le : m ≤ n) (hε : ε ≠ GeneType.NonPolarized) (hε' : ε' ≠ GeneType.NonPolarized) : ↑(Y10 h_le hε hε') = Gene.ofRank (2 * m) ε + Gene.ofRank (2 * n + 4) ε'

@[simp]

theorem MixPi2Lambda.neg_Y10 {ε ε' : GeneType} {m n : ℕ} (h_le : m ≤ n) (hε : ε ≠ GeneType.NonPolarized) (hε' : ε' ≠ GeneType.NonPolarized) : -Y10 h_le hε hε' = Y10 h_le ⋯ ⋯