ext_rat — Mathlib

English

If two monoid-with-zero homs from Rat agree on integers, they are equal.

Русский

Если два гомоморфизма из Rat совпадают на целых, они равны.

LaTeX

$$$\text{ext}_\text{rat}' : \forall f,g : ℚ →*₀ M₀,\ (\forall n ∈ \mathbb{Z}, f n = g n) \Rightarrow f = g.$$$

Lean4

/-- If monoid with zero homs `f` and `g` from `ℚ` agree on the integers then they are equal.

See note [partially-applied ext lemmas] for why `comp` is used here. -/
@[ext]
theorem ext_rat {f g : ℚ →*₀ M₀} (h : f.comp (Int.castRingHom ℚ : ℤ →*₀ ℚ) = g.comp (Int.castRingHom ℚ)) : f = g :=
  ext_rat' <| DFunLike.congr_fun h

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