exists_isMinimal — Mathlib

English

There exists a variable change C such that C • W is minimal over R.

Русский

Существует переменная смены C такая, что C • W минимальна по отношению к R.

LaTeX

$$$\\exists C : VariableChange K,\\; \\text{IsMinimal } R (C \\cdot W)$$$

Lean4

theorem exists_isMinimal (W : WeierstrassCurve K) : ∃ C : VariableChange K, IsMinimal R (C • W) :=
  by
  obtain ⟨C, hC⟩ :=
    exists_maximalFor_of_wellFoundedGT (fun (C : VariableChange K) ↦ IsIntegral R (C • W))
      (fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W)) (exists_isIntegral R W)
  refine ⟨C, ⟨⟨by simp only [one_smul, hC.1], ?_⟩⟩⟩
  intro j hj; rw [← smul_assoc] at hj
  let h := hC.2 hj
  simp_all only [one_smul]
  rw [← smul_assoc]
  exact h

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