instRingHomSurjectiveForallEvalRingHom

English

Let I be a (nonempty) index set and f : I → Type be semirings. For each i, the evaluation ring homomorphism Pi.evalRingHom f i : (∀ i, f i) →+* f i is surjective.

Русский

Пусть I непустой индекс. Для каждого i рассматривается выпуклое отображение Π.evalRingHom, и каждый evalRingHom является сюръективным.

LaTeX

$$$\\forall i, \\text{RingHomSurjective}(\\Pi.evalRingHom\\;f\\;i)$$$

Lean4

instance (f : I → Type*) [∀ i, Semiring (f i)] (i) : RingHomSurjective (Pi.evalRingHom f i) where
  is_surjective x := ⟨by classical exact (if h : · = i then h ▸ x else 0), by simp⟩

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