finCongr_symm_apply_coe

Mathlib.Data.Fin.SuccPred

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

English

For h : m = n and k : Fin n, ((finCongr h).symm k : ℕ) = k.

Русский

Для h : m = n и k : Fin n, ((finCongr h).symm k : ℕ) = k.

LaTeX

$$$$ ((\\mathrm{finCongr}(h).\\mathrm{symm})\\,k : \\mathbb{N}) = k. $$$$

Lean4

theorem _root_.finCongr_symm_apply_coe (h : m = n) (k : Fin n) : ((finCongr h).symm k : ℕ) = k :=
  rfl

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

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

Разделы

Аффилиация

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