nthHomSeq — Mathlib

English

The map nthHomSeq f_compat r is the sequence n ↦ nthHom f r n.

Русский

Гомоморф nthHomSeq f_compat r задаёт последовательность n ↦ nthHom f r n.

LaTeX

$$nthHomSeq (f) (r) : ℕ → ℤ := fun n => nthHom f r n$$

Lean4

/-- `nthHomSeq f_compat r` bundles `PadicInt.nthHom f r`
as a Cauchy sequence of rationals with respect to the `p`-adic norm.
The `n`th value of the sequence is `((f n r).val : ℚ)`.
-/
def nthHomSeq (r : R) : PadicSeq p :=
  ⟨fun n => nthHom f r n, isCauSeq_nthHom f_compat r⟩
    -- this lemma ran into issues after changing to `NeZero` and I'm not sure why.

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