map_mul' — Mathlib

English

The polynomial algebra F_q[X] embeds injectively into ringOfIntegers F_q F.

Русский

Алгебра многочленов F_q[X] инъективно включается в ringOfIntegers F_q F.

LaTeX

$$$\operatorname{algebraMap}_{F_q[X]} : F_q[X] \to \mathrm{ringOfIntegers}_{F_q}F \text{ is injective}.$$$

Lean4

theorem map_mul' (x y : RatFunc Fq) : inftyValuationDef Fq (x * y) = inftyValuationDef Fq x * inftyValuationDef Fq y :=
  by
  rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]
  by_cases hx : x = 0
  · rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
  · by_cases hy : y = 0
    · rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
    · simp_all [RatFunc.intDegree_mul]

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