changeLevel_eq_one_iff

Mathlib.NumberTheory.DirichletCharacter.Basic

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

← MathLib Explorer

English

For hm with n | m and m ≠ 0, changeLevel hm χ = 1 if and only if χ = 1.

Русский

При hm с n | m и m ≠ 0, changeLevel hm χ = 1 тогда и только тогда, когда χ = 1.

LaTeX

$$$$ changeLevel hm χ = 1 \\iff χ = 1. $$$$

Lean4

@[simp]
theorem changeLevel_eq_one_iff {m : ℕ} {χ : DirichletCharacter R n} (hm : n ∣ m) [NeZero m] :
    changeLevel hm χ = 1 ↔ χ = 1 :=
  map_eq_one_iff _ (changeLevel_injective hm)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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