rev_sub

Mathlib.Algebra.Group.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.rev_sub

English

For all a,b in Fin n, rev(a - b) = rev a + b.

Русский

Для любых a,b в Fin n, rev(a-b) = rev(a) + b.

LaTeX

$$$\\forall a,b\\in \\mathrm{Fin}(n),\\; \\mathrm{rev}(a-b)=\\mathrm{rev}(a)+b$$$

Lean4

theorem rev_sub (a b : Fin n) : rev (a - b) = rev a + b := by rw [rev_eq_iff, rev_add, rev_rev]

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

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

Разделы

Аффилиация

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