Documentation

Mathlib.Algebra.Group.Fin.Basic

Fin is a group #

This file contains the additive and multiplicative monoid instances on Fin n.

See note [foundational algebra order theory].

Instances #

instance Fin.addCommGroup (n : ) [NeZero n] :
Equations

Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

Equations

Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

Equations
  • =

Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

Equations

Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

Equations

Miscellaneous lemmas #

theorem Fin.coe_sub_one {n : } (a : Fin (n + 1)) :
(a - 1) = if a = 0 then n else a - 1
@[simp]
theorem Fin.lt_sub_one_iff {n : } {k : Fin (n + 2)} :
k < k - 1 k = 0
@[simp]
theorem Fin.le_sub_one_iff {n : } {k : Fin (n + 1)} :
k k - 1 k = 0
theorem Fin.sub_one_lt_iff {n : } {k : Fin (n + 1)} :
k - 1 < k 0 < k
@[simp]
theorem Fin.neg_last (n : ) :
theorem Fin.neg_natCast_eq_one (n : ) :
-n = 1