HepLean 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 #

source
instance Fin.addCommSemigroup (n : ℕ) :
AddCommSemigroup (Fin n)
Equations
source
instance Fin.instAddCommSemigroup (n : ℕ) :
AddCommSemigroup (Fin n)
Equations
source
instance Fin.addCommMonoid (n : ℕ) [NeZero n] :
AddCommMonoid (Fin n)
Equations
source
instance Fin.instAddMonoidWithOne (n : ℕ) [NeZero n] :
AddMonoidWithOne (Fin n)
Equations
source
instance Fin.addCommGroup (n : ℕ) [NeZero n] :
AddCommGroup (Fin n)
Equations
source
instance Fin.instInvolutiveNeg (n : ℕ) :
InvolutiveNeg (Fin n)

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

Equations
source
instance Fin.instIsCancelAdd (n : ℕ) :
IsCancelAdd (Fin n)

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

Equations
  • ⋯ = ⋯
source
instance Fin.instAddLeftCancelSemigroup (n : ℕ) :
AddLeftCancelSemigroup (Fin n)

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

Equations
source
instance Fin.instAddRightCancelSemigroup (n : ℕ) :
AddRightCancelSemigroup (Fin n)

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

Equations

Miscellaneous lemmas #

source
theorem Fin.coe_sub_one {n : ℕ} (a : Fin (n + 1)) :
↑(a - 1) = if a = 0 then n else ↑a - 1
source
@[simp]
theorem Fin.lt_sub_iff {n : ℕ} {a b : Fin n} :
a < a - b ↔ a < b
source
@[simp]
theorem Fin.sub_le_iff {n : ℕ} {a b : Fin n} :
a - b ≤ a ↔ b ≤ a
source
@[simp]
theorem Fin.lt_one_iff {n : ℕ} (x : Fin (n + 2)) :
x < 1 ↔ x = 0
source
theorem Fin.lt_sub_one_iff {n : ℕ} {k : Fin (n + 2)} :
k < k - 1 ↔ k = 0
source
@[simp]
theorem Fin.le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} :
k ≤ k - 1 ↔ k = 0
source
theorem Fin.sub_one_lt_iff {n : ℕ} {k : Fin (n + 1)} :
k - 1 < k ↔ 0 < k
source
@[simp]
theorem Fin.neg_last (n : ℕ) :
-Fin.last n = 1
source
theorem Fin.neg_natCast_eq_one (n : ℕ) :
-↑n = 1
source
theorem Fin.rev_add {n : ℕ} (a b : Fin n) :
(a + b).rev = a.rev - b
source
theorem Fin.rev_sub {n : ℕ} (a b : Fin n) :
(a - b).rev = a.rev + b
source
theorem Fin.add_lt_left_iff {n : ℕ} {a b : Fin n} :
a + b < a ↔ b.rev < a