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 #

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_iff {n : } {a : Fin n} {b : Fin n} :
a < a - b a < b
@[simp]
theorem Fin.sub_le_iff {n : } {a : Fin n} {b : Fin n} :
a - b a b a
@[simp]
theorem Fin.lt_one_iff {n : } (x : Fin (n + 2)) :
x < 1 x = 0
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
theorem Fin.rev_add {n : } (a : Fin n) (b : Fin n) :
(a + b).rev = a.rev - b
theorem Fin.rev_sub {n : } (a : Fin n) (b : Fin n) :
(a - b).rev = a.rev + b
theorem Fin.add_lt_left_iff {n : } {a : Fin n} {b : Fin n} :
a + b < a b.rev < a