changeLevel_factorsThrough — Mathlib

English

If hm : n ∣ m, then changeLevel hm χ factors through n, i.e., FactorsThrough (changeLevel hm χ) n

Русский

Если hm: n ∣ m, то changeLevel hm χ факторизуется через n: граф фактически FactorsThrough (changeLevel hm χ) n

LaTeX

$$$$ \\operatorname{FactorsThrough}(\\text{changeLevel}_{n\\to m}(χ))\\ n. $$$$

Lean4

theorem changeLevel_factorsThrough {m : ℕ} (hm : n ∣ m) : FactorsThrough (changeLevel hm χ) n :=
  ⟨hm, χ, rfl⟩

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