ext_rat_on_pnat — Mathlib

English

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

Русский

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

LaTeX

$$$\text{ext}_\text{rat on pnat} : \forall f,g : ℚ →*₀ M₀,\ (\forall n > 0, f n = g n) \Rightarrow f = g.$$$

Lean4

/-- If monoid with zero homs `f` and `g` from `ℚ` agree on the positive naturals and `-1` then
they are equal. -/
theorem ext_rat_on_pnat (same_on_neg_one : f (-1) = g (-1)) (same_on_pnat : ∀ n : ℕ, 0 < n → f n = g n) : f = g :=
  ext_rat' <|
    DFunLike.congr_fun <|
      show (f : ℚ →*₀ M₀).comp (Int.castRingHom ℚ : ℤ →*₀ ℚ) = (g : ℚ →*₀ M₀).comp (Int.castRingHom ℚ : ℤ →*₀ ℚ) from
        ext_int' (by simpa) (by simpa)

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