monoidWithZeroHom_ext — Mathlib

English

Two MonoidWithZeroHom from WithZero α to β that agree on the underlying monoid hom are equal; extensionality principle for WithZero.

Русский

Два MonoidWithZeroHom из WithZero α в β равны, если совпадают на сопряжённых множителях; принцип экстенсивности.

LaTeX

$$$f=g$ если их отображения на координатах совпадают; формально ext lemma$$

Lean4

@[ext high]
theorem monoidWithZeroHom_ext ⦃f g : WithZero α →*₀ β⦄
    (h : f.toMonoidHom.comp coeMonoidHom = g.toMonoidHom.comp coeMonoidHom) : f = g :=
  DFunLike.ext _ _ fun
    | 0 => (map_zero f).trans (map_zero g).symm
    | (g : α) => DFunLike.congr_fun h g

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