mult_comap_le — Mathlib

English

The multiplicity of the restricted place is at most that of the original place.

Русский

Множитель ограничения места не превосходит множителя исходного места.

LaTeX

$$$ \operatorname{mult}(w.\mathrm{comap} f) \leq \operatorname{mult}(w) $$$

Lean4

theorem mult_comap_le (f : k →+* K) (w : InfinitePlace K) : mult (w.comap f) ≤ mult w :=
  by
  rw [mult, mult]
  split_ifs with h₁ h₂ h₂
  pick_goal 3
  · exact (h₁ (h₂.comap _)).elim
  all_goals decide

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