changeLevel_self_toUnitHom — Mathlib

English

The self lift via changeLevel preserves the unit-hom: changeLevel_self_toUnitHom states (changeLevel (dvd_refl n) χ).toUnitHom = χ.toUnitHom.

Русский

Собственный подъём через смену уровня сохраняет отображение единиц: (changeLevel (dvd_refl n) χ).toUnitHom = χ.toUnitHom.

LaTeX

$$$$ (changeLevel (dvd\\_refl n) χ).toUnitHom = χ.toUnitHom. $$$$

Lean4

theorem changeLevel_self_toUnitHom : (changeLevel (dvd_refl n) χ).toUnitHom = χ.toUnitHom := by rw [changeLevel_self]

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