isDenseInducing_cast_withVal — Mathlib

English

The same construction is also dense inducing: the map above is dense inducing.

Русский

Та же конструкция также является плотной индукцией: отображение выше является плотной индукцией.

LaTeX

$$$IsDenseInducing\\left(\\operatorname{Rat.castHom}(\\mathbb{Q}_p) \\circ WithVal.equiv(\\operatorname{Rat.padicValuation}(p)) \\right)$$$

Lean4

theorem isDenseInducing_cast_withVal :
    IsDenseInducing ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) :=
  by
  refine Padic.isUniformInducing_cast_withVal.isDenseInducing ?_
  intro
    -- nhds_discrete causes timeouts on TC search

  simpa [-nhds_discrete] using Padic.denseRange_ratCast p _

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