conductor_le_conductor_mem_conductorSet

English

For any hd ∈ conductorSet χ, conductor χ ≤ conductor((Classical.choose hd.2).conductor).

Русский

Для любого hd ∈ conductorSet χ выполняется: conductor χ ≤ conductor((Classical.choose hd.2).conductor).

LaTeX

$$$\\forall {d}, (d \in \\operatorname{conductorSet}(\\chi)) \Rightarrow \\operatorname{conductor}(\\chi) \le \\operatorname{conductor}((\\text{Classical.choose } hd.2))$$$

Lean4

theorem conductor_le_conductor_mem_conductorSet {d : ℕ} (hd : d ∈ conductorSet χ) :
    χ.conductor ≤ (Classical.choose hd.2).conductor :=
  by
  refine
    Nat.sInf_le <|
      (mem_conductorSet_iff χ).mpr <|
        ⟨dvd_trans (conductor_dvd_level _) hd.1, (factorsThrough_conductor (Classical.choose hd.2)).2.choose, ?_⟩
  rw [changeLevel_trans _ (conductor_dvd_level _) hd.dvd, ←
    (factorsThrough_conductor (Classical.choose hd.2)).2.choose_spec]
  exact hd.eq_changeLevel

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