functions_ext — Mathlib

English

If two ring homomorphisms from a finite product are equal on all coordinate injections mulSingle i x, then they are equal.

Русский

Если два кольцевых гомоморфизма из произведения по всем координатам совпадают на каждом инжекте MulSingle i x, то они равны.

LaTeX

$$$$ \\forall i, x,\\; g(\\text{single}_i x) = h(\\text{single}_i x) \\Rightarrow g = h. $$$$

Lean4

@[ext]
theorem functions_ext [Finite I] (S : Type*) [NonAssocSemiring S] (g h : (∀ i, R i) →+* S)
    (H : ∀ (i : I) (x : R i), g (single i x) = h (single i x)) : g = h :=
  RingHom.coe_addMonoidHom_injective <| @AddMonoidHom.functions_ext I _ R _ _ S _ (g : (∀ i, R i) →+ S) h H

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