exists₂_genWeightSpace_smul_add_eq_bot

English

There exist integers p < 0 < q with genWeightSpaceSmulAdd = ⊥ at p and at q for χ1, χ2 with χ1 ≠ 0.

Русский

Существуют целые p < 0 < q такие, что весовые пространства для p и q пусты: genWeightSpaceSmulAdd = ⊥.

LaTeX

$$$\exists p<0,\; q>0: genWeightSpace(M, p \cdot χ_1 + χ_2) = ⊥ \land genWeightSpace(M, q \cdot χ_1 + χ_2) = ⊥$$$

Lean4

theorem exists₂_genWeightSpace_smul_add_eq_bot :
    ∃ᵉ (p < (0 : ℤ)) (q > (0 : ℤ)), genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧ genWeightSpace M (q • χ₁ + χ₂) = ⊥ :=
  by
  obtain ⟨q, hq₀, hq⟩ := exists_genWeightSpace_smul_add_eq_bot M χ₁ χ₂ hχ₁
  obtain ⟨p, hp₀, hp⟩ := exists_genWeightSpace_smul_add_eq_bot M (-χ₁) χ₂ (neg_ne_zero.mpr hχ₁)
  refine ⟨-(p : ℤ), by simpa, q, by simpa, ?_, ?_⟩
  · rw [neg_smul, ← smul_neg, natCast_zsmul]
    exact hp
  · rw [natCast_zsmul]
    exact hq

Похожие утверждения