ker_ringHom — Mathlib

English

For a family of semiring homomorphisms φi: S → Ri, the kernel of the product map φ: S → ∏ Ri equals the infimum of the individual kernels, i.e., ker(Pi.ringHom φ) = ⨅ i ker(φi).

Русский

Для семейства гомоморфизмов φi: S → Ri, ядро произведения равно пересечению (инфимууму) ядер отдельных гомоморфизмов: ker(Pi.ringHom φ) = ⨅ i ker(φi).

LaTeX

$$$\\ker (\\Pi \\text{ringHom } \\varphi) = \\bigcap_i \\ker (\\varphi_i)$$$

Lean4

theorem _root_.Pi.ker_ringHom {ι : Type*} {R : ι → Type*} [∀ i, Semiring (R i)] (φ : ∀ i, S →+* R i) :
    ker (Pi.ringHom φ) = ⨅ i, ker (φ i) := by
  ext x
  simp [mem_ker, funext_iff]

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