toUnitHom_inj — Mathlib

English

The map that raises the level along n | m is injective (assuming the target level m is nonzero).

Русский

Ом функция повышения уровня по правилу n | m является инъективной (если m ≠ 0).

LaTeX

$$$$\\operatorname{changeLevel}(R := R)\\; hm:\\; \\mathrm{DirichletCharacter}\\; R\\; n \\to\\; \\mathrm{DirichletCharacter}\\; R\\; m \\text{ is injective when } m \\neq 0.$$$$

Lean4

theorem toUnitHom_inj (ψ : DirichletCharacter R n) : toUnitHom χ = toUnitHom ψ ↔ χ = ψ := by simp

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