ext_nnrat_on_pnat — Mathlib

English

If p.den and q.den cast to α are nonzero, then the cast of p − q equals p − q in α.

Русский

Если p.den и q.den приводятся в α ненулевыми, то приведение p − q равно p − q в α.

LaTeX

$$$\forall p,q \in \mathbb{Q},\ (p.den : \alpha) \neq 0 \land (q.den : \alpha) \neq 0 \Rightarrow ↑(p - q) = (p - q : \alpha).$$$

Lean4

/-- If monoid with zero homs `f` and `g` from `ℚ≥0` agree on the positive naturals then they are
equal. -/
theorem ext_nnrat_on_pnat (same_on_pnat : ∀ n : ℕ, 0 < n → f n = g n) : f = g :=
  ext_nnrat' <|
    DFunLike.congr_fun <|
      ext_nat'' ((f : ℚ≥0 →*₀ M₀).comp (Nat.castRingHom ℚ≥0 : ℕ →*₀ ℚ≥0))
        ((g : ℚ≥0 →*₀ M₀).comp (Nat.castRingHom ℚ≥0 : ℕ →*₀ ℚ≥0)) (by simpa)

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