existsUnique — Mathlib

English

χ factors through d if and only if the unit-map ker of ZMod d is contained in ker of χ.toUnitHom.

Русский

χ факторизуется через d тогда и только тогда, когда ker ZMod d вложено в ker χ.toUnitHom.

LaTeX

$$$$ \\operatorname{FactorsThrough}(χ,d) \\iff \\ker(\\mathrm{ZMod.unitsMap}(d)) \\le \\ker(χ^{\\mathrm{toUnitHom}}). $$$$

Lean4

/-- The character of level `d` through which `χ` factors is uniquely determined. -/
theorem existsUnique {d : ℕ} [NeZero n] (h : FactorsThrough χ d) :
    ∃! χ' : DirichletCharacter R d, χ = changeLevel h.dvd χ' :=
  by
  rcases h with ⟨hd, χ₂, rfl⟩
  exact ⟨χ₂, rfl, fun χ₃ hχ₃ ↦ (changeLevel_injective hd hχ₃).symm⟩

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