ext_nnrat' — Mathlib

English

For p ∈ ℚ and n ∈ ℕ, the cast of p^n equals (p^n) cast in α.

Русский

Для p ∈ ℚ и n ∈ ℕ приводение p^n в α даёт тот же результат, что и (p^n) в α.

LaTeX

$$$\forall p \in \mathbb{Q}, \forall n \in \mathbb{N},\ ↑(p^n) = (p^n : \alpha).$$$

Lean4

/-- If monoid with zero homs `f` and `g` from `ℚ≥0` agree on the naturals then they are equal. -/
theorem ext_nnrat' (h : ∀ n : ℕ, f n = g n) : f = g :=
  (DFunLike.ext f g) fun r =>
    by
    rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, eq_on_inv₀ f g]
    apply h

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