mk_zero_right — Mathlib

English

An inductive lemma showing higher-right-zero cases reduce to zero via Frobenius action.

Русский

Индуктивная лемма, показывающая, что правый ноль в более общего случая сводится к нулю через действие Фробениуса.

LaTeX

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

Lean4

@[simp]
theorem mk_zero_right (n : ℕ) : mk K p (n, 0) = 0 := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [← ih]
    apply (Quot.sound _).symm
    have := R.intro (p := p) n (0 : K)
    rwa [frobenius_zero K p] at this

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