twoTorsionPolynomial_disc_isUnit — Mathlib

English

If 2 is a unit in R, then W.twoTorsionPolynomial.disc is a unit iff W.Δ is a unit: IsUnit(W.twoTorsionPolynomial.disc) ↔ IsUnit(W.Δ).

Русский

Если 2 является единицей в R, то IsUnit(W.twoTorsionPolynomial.disc) эквивалентно IsUnit(W.Δ).

LaTeX

$$$ \mathrm{IsUnit}(W.twoTorsionPolynomial.disc) \iff \mathrm{IsUnit}(W.\Delta) $$$

Lean4

theorem twoTorsionPolynomial_disc_isUnit (hu : IsUnit (2 : R)) : IsUnit W.twoTorsionPolynomial.disc ↔ IsUnit W.Δ :=
  by
  rw [twoTorsionPolynomial_disc, IsUnit.mul_iff, show (16 : R) = 2 ^ 4 by norm_num1]
  exact
    and_iff_right <|
      hu.pow
        4
          -- TODO: change to `[IsUnit ...]` once https://github.com/leanprover-community/mathlib4/issues/17458 is merged
          -- TODO: In this case `IsUnit W.Δ` is just `W.IsElliptic`, consider removing/rephrasing this result

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