mk_ψ₂_sq — Mathlib

English

The square of the coordinate in the coordinate ring corresponding to ψ₂ equals the coordinate corresponding to C Ψ₂Sq.

Русский

Квадрат координаты в кольце координат, соответствующий ψ₂, равен координате, соответствующей C Ψ₂Sq.

LaTeX

$$$$\operatorname{mk}(W, W.\psi_2)^2 = \operatorname{mk}(W, C(W.\Psi_2Sq)).$$$$

Lean4

theorem mk_ψ₂_sq : mk W W.ψ₂ ^ 2 = mk W (C W.Ψ₂Sq) := by
  simp [C_Ψ₂Sq]
    -- TODO: remove `twoTorsionPolynomial` in favour of `Ψ₂Sq`

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