sound — Mathlib

English

Soundness of the R-structure under iteration of Frobenius in the PerfectClosure context, formalized by a commuting diagram.

Русский

Корректность структуры R при повторной итерации Frobenius в контексте PerfectClosure, закодированная диаграммой коммутирования.

LaTeX

$$Soundness relation for PerfectClosure.R$$

Lean4

theorem sound (m n : ℕ) (x y : K) (H : (frobenius K p)^[m] x = y) : mk K p (n, x) = mk K p (m + n, y) :=
  by
  subst H
  induction m with
  | zero => simp only [zero_add, iterate_zero_apply]
  | succ m ih =>
    rw [ih, Nat.succ_add, iterate_succ']
    apply Quot.sound
    apply R.intro

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