associated_of_isUniformizer — Mathlib

English

If two elements are uniformizers, they are associated.

Русский

Если два элемента являются uniformizers, они ассоциированы.

LaTeX

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

Lean4

/-- If two elements of `K₀` are uniformizers, then they are associated. -/
theorem associated_of_isUniformizer {π₁ π₂ : K₀} (h1 : IsUniformizer v π₁) (h2 : IsUniformizer v π₂) :
    Associated π₁ π₂ :=
  by
  have hval : v ((π₁ : K)⁻¹ * π₂) = 1 := by simp [IsUniformizer.iff.mp h1, IsUniformizer.iff.mp h2]
  set p : v.integer := ⟨(π₁.1 : K)⁻¹ * π₂.1, (v.mem_integer_iff _).mpr (le_of_eq hval)⟩ with hp
  use ((Integers.isUnit_iff_valuation_eq_one (x := p) <| integer.integers v).mpr hval).unit
  apply_fun ((↑) : K₀ → K) using Subtype.val_injective
  simp [hp, ← mul_assoc, mul_inv_cancel₀ h1.ne_zero]

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