same_level

Mathlib.NumberTheory.DirichletCharacter.Basic

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.FactorsThrough.same_level

English

For any χ, FactorsThrough χ n holds; i.e., χ factors through its own level.

Русский

Для любого χ выполняется, что χ факторизуется через уровень n; χ имеет собственный уровень.

LaTeX

$$$$ \\mathrm{FactorsThrough}(χ, n). $$$$

Lean4

theorem same_level : FactorsThrough χ n :=
  ⟨dvd_refl n, χ, (changeLevel_self χ).symm⟩

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

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

Разделы

Аффилиация

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