mk_φ — Mathlib

English

In the affine coordinate ring, mk_W(W.φ(n)) = mk_W(C Φ(n)); i.e., the mk-images of φ and Φ coincide.

Русский

В аффинном координатном кольце mk_W(W.φ(n)) = mk_W(C Φ(n)); изображение mk φ совпадает с изображением Φ.

LaTeX

$$$\\operatorname{mk}_W\\big(W.\\phi(n)\\big) = \\operatorname{mk}_W\\big(C(\\Phi(n))\\big)$$$

Lean4

theorem mk_φ (n : ℤ) : mk W (W.φ n) = mk W (C <| W.Φ n) := by
  simp_rw [φ, Φ, map_sub, map_mul, map_pow, mk_ψ, mk_Ψ_sq, Ψ, map_mul, mul_mul_mul_comm _ <| mk W <| ite ..,
    Int.even_add_one, Int.even_sub_one, ite_not, ← sq, apply_ite C, apply_ite <| mk W, ite_pow, map_one, one_pow,
    mk_ψ₂_sq]

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