changeLevel_injective — Mathlib

English

The changeLevel map is injective; if changeLevel hm χ = changeLevel hm ψ, then χ = ψ.

Русский

Функция повышения уровня инъективна: если их образы совпадают, то сами χ и ψ равны.

LaTeX

$$$$ \\forall \\chi,\\psi,\\; (changeLevel hm χ = changeLevel hm ψ) \\Rightarrow χ = ψ.$$$$

Lean4

/-- The `changeLevel` map is injective (except in the degenerate case `m = 0`). -/
theorem changeLevel_injective {m : ℕ} [NeZero m] (hm : n ∣ m) : Function.Injective (changeLevel (R := R) hm) :=
  by
  intro _ _ h
  ext1 y
  obtain ⟨z, rfl⟩ := ZMod.unitsMap_surjective hm y
  rw [MulChar.ext_iff] at h
  simpa [changeLevel_def] using h z

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