iInf_ker_truncate — Mathlib

English

The infimum of the kernels of WittVector.truncate over all i is the zero submodule: ⨅ i, RingHom.ker (WittVector.truncate (p := p) (R := R) i) = ⊥.

Русский

Первая общая граница ядер виттового усечения равна ⊥.

LaTeX

$$$$\\bigwedge_{i:\\mathbb{N}} \\ker\\bigl(\\mathrm{WittVector.truncate}(p := p)(R := R) i\\bigr) = \\{0\\}. $$$$

Lean4

theorem iInf_ker_truncate : ⨅ i : ℕ, RingHom.ker (WittVector.truncate (p := p) (R := R) i) = ⊥ :=
  by
  rw [Submodule.eq_bot_iff]
  intro x hx
  ext
  simp only [WittVector.mem_ker_truncate, Ideal.mem_iInf, WittVector.zero_coeff] at hx ⊢
  exact hx _ _ (Nat.lt_succ_self _)

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