mk_zero — Mathlib

English

For every n, mk K p (n, 0) = 0 in PerfectClosure K p; i.e., the right zero is sent to zero via Frobenius consistency.

Русский

Для каждого n выполняется mk K p (n, 0) = 0 в PerfectClosure K p.

LaTeX

$$mk K p (n, 0) = 0$$

Lean4

/-- Prior to https://github.com/leanprover-community/mathlib4/pull/15862, this lemma was called `mk_zero_zero`.
See `mk_zero_right` for the lemma used to be called `mk_zero`. -/
@[simp]
theorem mk_zero : mk K p 0 = 0 :=
  rfl

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