of_associated — Mathlib

English

If π1 is a uniformizer and π2 is associated to π1, then π2 is also a uniformizer.

Русский

Если π1 — uniformizer и π2 ассоциирован с π1, то π2 тоже uniformizer.

LaTeX

$$v.IsUniformizer π₁ ∧ Associated π₁ π₂ → v.IsUniformizer π₂$$

Lean4

/-- An element associated to a uniformizer is itself a uniformizer. -/
theorem of_associated {π₁ π₂ : K₀} (h1 : IsUniformizer v π₁) (H : Associated π₁ π₂) : IsUniformizer v π₂ :=
  by
  obtain ⟨u, hu⟩ := H
  have : v (u.1 : K) = 1 := (Integers.isUnit_iff_valuation_eq_one <| integer.integers v).mp u.isUnit
  rwa [IsUniformizer.iff, ← hu, Subring.coe_mul, map_mul, this, mul_one, ← IsUniformizer.iff]

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