norm_eq_norm_app_of_nonzero — Mathlib

English

For a nonzero PadicSeq f, there exists a k such that f.norm = padicNorm p k and k ≠ 0.

Русский

Для ненулевой PadicSeq f существует k с f.norm = padicNorm p k и k ≠ 0.

LaTeX

$$∃ k, f.norm = padicNorm p k ∧ k ≠ 0$$

Lean4

theorem norm_eq_norm_app_of_nonzero {f : PadicSeq p} (hf : ¬f ≈ 0) : ∃ k, f.norm = padicNorm p k ∧ k ≠ 0 :=
  have heq : f.norm = padicNorm p (f <| stationaryPoint hf) := by simp [norm, hf]
  ⟨f <| stationaryPoint hf, heq, fun h ↦ norm_nonzero_of_not_equiv_zero hf (by simpa [h] using heq)⟩

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