padicValRat_of_nat — Mathlib

English

There is a direct equality between padicValNat p n and padicValRat p n.cast, i.e., ↑padicValNat p n = padicValRat p n.cast.

Русский

Существует прямое соответствие: ↑padicValNat p n = padicValRat p n.cast.

LaTeX

$$$\uparrow\mathrm{padicValNat}(p,n) = \mathrm{padicValRat}(p,n.cast)$$$

Lean4

/-- `padicValRat` coincides with `padicValNat`. -/
@[norm_cast]
theorem padicValRat_of_nat (n : ℕ) : ↑(padicValNat p n) = padicValRat p n := by simp

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