ext_nnrat — Mathlib

English

For n ∈ ℕ, the inverse of n in ℚ, cast to α, equals the inverse of n in α.

Русский

Для n ∈ ℕ обратное к n в ℚ, приводимое к α, равно обратному к n в α.

LaTeX

$$$\forall n \in \mathbb{N},\ ↑(n^{-1}) = (n)^{-1}.$$$

Lean4

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

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

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