image' — Mathlib

English

Division is preserved by the embedding: the map respects division.

Русский

Встраивание сохраняет деление: отображение сохраняет деление.

LaTeX

$$$\\uparrow(x/y) = \\uparrow x / \\uparrow y$$$

Lean4

protected theorem image' {q : ℚ_[p]} : q ≠ 0 → ∃ n : ℤ, padicNormE q = (p : ℚ) ^ (-n) :=
  Quotient.inductionOn q fun f hf ↦
    have : ¬f ≈ 0 := (ne_zero_iff_nequiv_zero f).1 hf
    norm_values_discrete f this

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