comap_mulValuation_eq_int_padicValuation

English

The comap of mulValuation along Int.castRingHom agrees with Int.padicValuation.

Русский

Комап mulValuation по Int.castRingHom совпадает с Int.padicValuation.

LaTeX

$$mulValuation.comap(Int.castRingHom) = Int.padicValuation(p)$$

Lean4

theorem comap_mulValuation_eq_int_padicValuation :
    (mulValuation (p := p)).comap (Int.castRingHom _) = Int.padicValuation p :=
  by
  ext
  simp [← Rat.padicValuation_cast, ← comap_mulValuation_eq_padicValuation]

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