instForall — Mathlib

English

If every component f(i) is formally unramified over R, then the Pi-type Π i, f i is formally unramified over R.

Русский

Если каждый компонент f(i) формально неразветвлен над R, тогда Π i, f i формально неразветвлен над R.

LaTeX

$$$[\\forall i,\\; \\mathrm{Algebra.FormallyUnramified}\\; R\\; (f\\,i)]\\;\\Rightarrow\\; \\mathrm{Algebra.FormallyUnramified}\\; R\\; ((i:\\,I) \\to f\\,i).$$$

Lean4

instance [∀ i, FormallyUnramified R (f i)] : FormallyUnramified R (Π i, f i) :=
  (pi_iff _).mpr ‹_›

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