neg_natCast_eq_one

Mathlib.Algebra.Group.Fin.Basic

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

English

Fin(n) with addition is AddRightCancelSemigroup.

Русский

Fin(n) с операцией сложения образует AddRightCancelSemigroup.

LaTeX

$$$\\forall n\\, \\operatorname{AddRightCancelSemigroup}(\\mathrm{Fin}(n))$$$

Lean4

theorem neg_natCast_eq_one (n : ℕ) : -(n : Fin (n + 1)) = 1 := by simp only [natCast_eq_last, neg_last]

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

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

Разделы

Аффилиация

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