English
The product of two canonical elements mk x and mk y equals the canonical element with coordinates x.fst+y.fst and snd given by the Frobenius-shifted components, precisely as in the lifting definition.
Русский
Произведение двух канонических элементов mk x и mk y равно каноническому элементу с координатами x.fst+y.fst и вторым компонентом, полученным после сдвига по Фробениусу.
LaTeX
$$$mk\\,K\\,p\\,x * mk\\,K\\,p\\,y = mk\\,K\\,p\\big( x.1+y.1, (\\mathrm{frobenius}\\,K\\,p)^{[y.1]} x.2 \\cdot (\\mathrm{frobenius}\\,K\\,p)^{[x.1]} y.2 \\big)$$$
Lean4
@[simp]
theorem mk_mul_mk (x y : ℕ × K) :
mk K p x * mk K p y = mk K p (x.1 + y.1, (frobenius K p)^[y.1] x.2 * (frobenius K p)^[x.1] y.2) :=
rfl
