finCongr_symm

Mathlib.Data.Fin.SuccPred

URI: https://scilib.ai/kg/mathlib#finCongr_symm

English

If h : m = n, then the inverse of finCongr h is finCongr h.symm.

Русский

Если h : m = n, то обратное отображение finCongr h равно finCongr h.symm.

LaTeX

$$$$ (\\mathrm{finCongr}(h))^{-1} = \\mathrm{finCongr}(h^{\\mathrm{symm}}). $$$$

Lean4

@[simp]
theorem _root_.finCongr_symm (h : m = n) : (finCongr h).symm = finCongr h.symm :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru