twoTorsionPolynomial_disc_ne_zero

English

If R is nontrivial, 2 is a unit in R, and W.Δ is a unit, then W.twoTorsionPolynomial.disc ≠ 0.

Русский

Если R не тривиально, 2 — единица в R, и W.Δ — единица, то W.twoTorsionPolynomial.disc ≠ 0.

LaTeX

$$$ W.twoTorsionPolynomial.disc \neq 0 $$$

Lean4

theorem twoTorsionPolynomial_disc_ne_zero [Nontrivial R] (hu : IsUnit (2 : R)) (hΔ : IsUnit W.Δ) :
    W.twoTorsionPolynomial.disc ≠ 0 :=
  ((W.twoTorsionPolynomial_disc_isUnit hu).mpr hΔ).ne_zero

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