mem_conductorSet_dvd

Mathlib.NumberTheory.DirichletCharacter.Basic

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.mem_conductorSet_dvd

English

If x ∈ conductorSet χ, then x divides n.

Русский

Если x ∈ conductorSet χ, то x делит n.

LaTeX

$$$x \in \operatorname{conductorSet}(\\chi) \\Rightarrow x \mid n$$$

Lean4

theorem mem_conductorSet_dvd {x : ℕ} (hx : x ∈ conductorSet χ) : x ∣ n :=
  hx.dvd

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru