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.addCommSemigroup (n : ) :
Equations
instance Fin.instAddCommSemigroup (n : ) :
Equations
instance Fin.addCommMonoid (n : ) [] :
Equations
• = let __spread.0 := ;
instance Fin.instAddMonoidWithOne (n : ) [] :
Equations
• = let __spread.0 := ;
instance Fin.addCommGroup (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
• = let __src := ; let __src_1 := ;

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

Equations
• = let __src := ; let __src_1 := ;

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 : ) :
= 1
theorem Fin.neg_natCast_eq_one (n : ) :
-n = 1