Mathlib.Algebra.Group.Fin.Basic

Fin.addCommSemigroup instance

(n : ℕ) : AddCommSemigroup (Fin n)

Full source

instance addCommSemigroup (n : ℕ) : AddCommSemigroup (Fin n) where
  add_assoc := by simp [Fin.ext_iff, add_def, Nat.add_assoc]
  add_comm := by simp [Fin.ext_iff, add_def, Nat.add_comm]

Additive Commutative Semigroup Structure on Finite Types

Informal description

For any natural number $n$, the finite type $\mathrm{Fin}\,n$ forms an additive commutative semigroup.

Fin.instAddCommSemigroup instance

(n) : AddCommSemigroup (Fin n)

Full source

instance (n) : AddCommSemigroup (Fin n) where
  add_assoc := by simp [Fin.ext_iff, add_def, Nat.add_assoc]
  add_comm := by simp [Fin.ext_iff, add_def, add_comm]

Additive Commutative Semigroup Structure on Finite Types

Informal description

For any natural number $n$, the finite type $\mathrm{Fin}(n)$ (the set $\{0, 1, \dots, n-1\}$) forms an additive commutative semigroup under addition modulo $n$.

Fin.addCommMonoid instance

(n : ℕ) [NeZero n] : AddCommMonoid (Fin n)

Full source

instance addCommMonoid (n : ℕ) [NeZero n] : AddCommMonoid (Fin n) where
  zero_add := Fin.zero_add
  add_zero := Fin.add_zero
  nsmul := nsmulRec
  __ := Fin.addCommSemigroup n

Additive Commutative Monoid Structure on Finite Types

Informal description

For any natural number $n \neq 0$, the finite type $\mathrm{Fin}\,n$ (the set $\{0, 1, \dots, n-1\}$) forms an additive commutative monoid under addition modulo $n$.

Fin.instAddMonoidWithOne instance

(n) [NeZero n] : AddMonoidWithOne (Fin n)

Full source

instance instAddMonoidWithOne (n) [NeZero n] : AddMonoidWithOne (Fin n) where
  __ := inferInstanceAs (AddCommMonoid (Fin n))
  natCast i := Fin.ofNat' n i
  natCast_zero := rfl
  natCast_succ _ := Fin.ext (add_mod _ _ _)

Additive Monoid with One Structure on Finite Types

Informal description

For any nonzero natural number $n$, the finite type $\mathrm{Fin}(n)$ (the set $\{0, 1, \dots, n-1\}$) forms an additive monoid with a distinguished element $1$ and a canonical homomorphism from the natural numbers, where addition is performed modulo $n$.

Fin.addCommGroup instance

(n : ℕ) [NeZero n] : AddCommGroup (Fin n)

Full source

instance addCommGroup (n : ℕ) [NeZero n] : AddCommGroup (Fin n) where
  __ := addCommMonoid n
  __ := neg n
  neg_add_cancel := fun ⟨a, ha⟩ ↦
    Fin.ext <| (Nat.mod_add_mod _ _ _).trans <| by
      rw [Fin.val_zero, Nat.sub_add_cancel, Nat.mod_self]
      exact le_of_lt ha
  sub := Fin.sub
  sub_eq_add_neg := fun ⟨a, ha⟩ ⟨b, hb⟩ ↦
    Fin.ext <| by simp [Fin.sub_def, Fin.neg_def, Fin.add_def, Nat.add_comm]
  zsmul := zsmulRec

Additive Commutative Group Structure on Finite Types $\mathrm{Fin}(n)$

Informal description

For any nonzero natural number $n$, the finite type $\mathrm{Fin}(n)$ (the set $\{0, 1, \dots, n-1\}$) forms an additive commutative group under addition modulo $n$.

Fin.instInvolutiveNeg instance

(n : ℕ) : InvolutiveNeg (Fin n)

Full source

/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
instance instInvolutiveNeg (n : ℕ) : InvolutiveNeg (Fin n) where
  neg_neg := Nat.casesOn n finZeroElim fun _i ↦ neg_neg

Involutive Negation on Finite Types $\mathrm{Fin}(n)$

Informal description

For any natural number $n$, the negation operation on $\mathrm{Fin}(n)$ is involutive, meaning that $-(-a) = a$ for all $a \in \mathrm{Fin}(n)$.

Fin.instIsCancelAdd instance

(n : ℕ) : IsCancelAdd (Fin n)

Full source

/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
instance instIsCancelAdd (n : ℕ) : IsCancelAdd (Fin n) where
  add_left_cancel := Nat.casesOn n finZeroElim fun _i _ _ _ ↦ add_left_cancel
  add_right_cancel := Nat.casesOn n finZeroElim fun _i _ _ _ ↦ add_right_cancel

Cancellative Addition on Finite Types $\mathrm{Fin}(n)$

Informal description

For any natural number $n$, the addition operation on $\mathrm{Fin}(n)$ is cancellative. That is, for any $a, b, c \in \mathrm{Fin}(n)$, if $a + b = a + c$ or $b + a = c + a$, then $b = c$.

Fin.instAddLeftCancelSemigroup instance

(n : ℕ) : AddLeftCancelSemigroup (Fin n)

Full source

/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
instance instAddLeftCancelSemigroup (n : ℕ) : AddLeftCancelSemigroup (Fin n) :=
  { Fin.addCommSemigroup n, Fin.instIsCancelAdd n with }

Additive Left Cancellative Semigroup Structure on Finite Types $\mathrm{Fin}(n)$

Informal description

For any natural number $n$, the finite type $\mathrm{Fin}\,n$ forms an additive left cancellative semigroup. That is, for any $a, b, c \in \mathrm{Fin}\,n$, if $a + b = a + c$, then $b = c$.

Fin.instAddRightCancelSemigroup instance

(n : ℕ) : AddRightCancelSemigroup (Fin n)

Full source

/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
instance instAddRightCancelSemigroup (n : ℕ) : AddRightCancelSemigroup (Fin n) :=
  { Fin.addCommSemigroup n, Fin.instIsCancelAdd n with }

Right Cancellative Addition on Finite Types $\mathrm{Fin}(n)$

Informal description

For any natural number $n$, the finite type $\mathrm{Fin}\,n$ forms a right cancellative additive semigroup. That is, for any $a, b, c \in \mathrm{Fin}\,n$, if $b + a = c + a$, then $b = c$.

Fin.coe_sub_one theorem

(a : Fin (n + 1)) : ↑(a - 1) = if a = 0 then n else a - 1

Full source

lemma coe_sub_one (a : Fin (n + 1)) : ↑(a - 1) = if a = 0 then n else a - 1 := by
  cases n
  · simp
  split_ifs with h
  · simp [h]
  rw [sub_eq_add_neg, val_add_eq_ite, coe_neg_one, if_pos, Nat.add_comm, Nat.add_sub_add_left]
  conv_rhs => rw [Nat.add_comm]
  rw [Nat.add_le_add_iff_left, Nat.one_le_iff_ne_zero]
  rwa [Fin.ext_iff] at h

Value of Subtracting One in $\mathrm{Fin}(n+1)$: $\text{val}(a - 1) = n$ if $a = 0$, else $a - 1$

Informal description

For any element $a$ in the finite type $\mathrm{Fin}(n+1)$, the natural number value of $a - 1$ is given by: \[ \text{val}(a - 1) = \begin{cases} n & \text{if } a = 0, \\ a - 1 & \text{otherwise.} \end{cases} \] Here, $\text{val}(x)$ denotes the underlying natural number value of $x \in \mathrm{Fin}(n+1)$.

Fin.lt_sub_iff theorem

{n : ℕ} {a b : Fin n} : a < a - b ↔ a < b

Full source

@[simp]
lemma lt_sub_iff {n : ℕ} {a b : Fin n} : a < a - b ↔ a < b := by
  rcases n with - | n
  · exact a.elim0
  constructor
  · contrapose!
    intro h
    obtain ⟨l, hl⟩ := Nat.exists_eq_add_of_le (Fin.not_lt.mp h)
    simpa only [Fin.not_lt, le_iff_val_le_val, sub_def, hl, ← Nat.add_assoc, Nat.add_mod_left,
      Nat.mod_eq_of_lt, Nat.sub_add_cancel b.is_lt.le] using
        (le_trans (mod_le _ _) (le_add_left _ _))
  · intro h
    rw [lt_iff_val_lt_val, sub_def]
    simp only
    obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt b.is_lt
    have : n + 1 - b = k + 1 := by
      simp_rw [hk, Nat.add_assoc, Nat.add_sub_cancel_left]
      -- simp_rw because, otherwise, rw tries to rewrite inside `b : Fin (n + 1)`
    rw [this, Nat.mod_eq_of_lt (hk.ge.trans_lt' ?_), Nat.lt_add_left_iff_pos] <;>
    omega

Inequality Characterization of Subtraction in Finite Types

Informal description

For any natural number $n$ and elements $a, b$ in the finite type $\text{Fin}(n)$, the inequality $a < a - b$ holds if and only if $a < b$.

Fin.sub_le_iff theorem

{n : ℕ} {a b : Fin n} : a - b ≤ a ↔ b ≤ a

Full source

@[simp]
lemma sub_le_iff {n : ℕ} {a b : Fin n} : a - b ≤ a ↔ b ≤ a := by
  rw [← not_iff_not, Fin.not_le, Fin.not_le, lt_sub_iff]

Subtraction Preserves Order in Finite Types: $a - b \leq a \leftrightarrow b \leq a$

Informal description

For any natural number $n$ and elements $a, b$ in the finite type $\mathrm{Fin}(n)$, the inequality $a - b \leq a$ holds if and only if $b \leq a$.

Fin.lt_one_iff theorem

{n : ℕ} (x : Fin (n + 2)) : x < 1 ↔ x = 0

Full source

@[simp]
lemma lt_one_iff {n : ℕ} (x : Fin (n + 2)) : x < 1 ↔ x = 0 := by
  simp [lt_iff_val_lt_val]

Characterization of Zero in $\text{Fin}(n+2)$ via Strict Inequality with One

Informal description

For any natural number $n$ and any element $x$ in the finite type $\text{Fin}(n+2)$, the inequality $x < 1$ holds if and only if $x = 0$.

Fin.lt_sub_one_iff theorem

{k : Fin (n + 2)} : k < k - 1 ↔ k = 0

Full source

lemma lt_sub_one_iff {k : Fin (n + 2)} : k < k - 1 ↔ k = 0 := by
  simp

Characterization of elements in $\mathrm{Fin}(n+2)$ satisfying $k < k - 1$

Informal description

For any element $k$ in the finite type $\mathrm{Fin}(n+2)$, the inequality $k < k - 1$ holds if and only if $k = 0$.

Fin.le_sub_one_iff theorem

{k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0

Full source

@[simp] lemma le_sub_one_iff {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 := by
  cases n
  · simp [fin_one_eq_zero k]
  simp only [le_def]
  rw [← lt_sub_one_iff, le_iff_lt_or_eq, val_fin_lt, val_inj, lt_sub_one_iff, or_iff_left_iff_imp,
    eq_comm, sub_eq_iff_eq_add]
  simp

Characterization of Zero in $\mathrm{Fin}(n+1)$ via Non-Strict Inequality with Predecessor

Informal description

For any element $k$ in the finite type $\mathrm{Fin}(n+1)$, the inequality $k \leq k - 1$ holds if and only if $k = 0$.

Fin.sub_one_lt_iff theorem

{k : Fin (n + 1)} : k - 1 < k ↔ 0 < k

Full source

lemma sub_one_lt_iff {k : Fin (n + 1)} : k - 1 < k ↔ 0 < k :=
  not_iff_not.1 <| by simp only [lt_def, not_lt, val_fin_le, le_sub_one_iff, le_zero_iff]

Subtraction Inequality in Finite Types: $k - 1 < k \leftrightarrow 0 < k$

Informal description

For any element $k$ in the finite type $\mathrm{Fin}(n+1)$, the inequality $k - 1 < k$ holds if and only if $0 < k$.

Fin.neg_last theorem

(n : ℕ) : -Fin.last n = 1

Full source

@[simp] lemma neg_last (n : ℕ) : -Fin.last n = 1 := by simp [neg_eq_iff_add_eq_zero]

Negation of Last Element in $\mathrm{Fin}(n+1)$ Equals One

Informal description

For any natural number $n$, the negation of the last element in $\mathrm{Fin}(n+1)$ (i.e., $-(\mathrm{last}\,n)$) equals $1$.

Fin.neg_natCast_eq_one theorem

(n : ℕ) : -(n : Fin (n + 1)) = 1

Full source

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

Negation of Cast $n$ in $\mathrm{Fin}(n+1)$ Equals One

Informal description

For any natural number $n$, the negation of the canonical casting of $n$ into $\mathrm{Fin}(n+1)$ equals $1$, i.e., $- (n : \mathrm{Fin}(n+1)) = 1$.

Fin.rev_add theorem

(a b : Fin n) : rev (a + b) = rev a - b

Full source

lemma rev_add (a b : Fin n) : rev (a + b) = rev a - b := by
  cases n
  · exact a.elim0
  rw [← last_sub, ← last_sub, sub_add_eq_sub_sub]

Reverse of Sum Equals Reverse Minus in $\mathrm{Fin}(n)$

Informal description

For any elements $a$ and $b$ of the finite type $\mathrm{Fin}(n)$, the reverse of their sum equals the reverse of $a$ minus $b$, i.e., $\mathrm{rev}(a + b) = \mathrm{rev}(a) - b$.

Fin.rev_sub theorem

(a b : Fin n) : rev (a - b) = rev a + b

Full source

lemma rev_sub (a b : Fin n) : rev (a - b) = rev a + b := by
  rw [rev_eq_iff, rev_add, rev_rev]

Reverse of Difference Equals Reverse Plus in $\mathrm{Fin}(n)$

Informal description

For any elements $a$ and $b$ of the finite type $\mathrm{Fin}(n)$, the reverse of their difference equals the reverse of $a$ plus $b$, i.e., $\mathrm{rev}(a - b) = \mathrm{rev}(a) + b$.

Fin.add_lt_left_iff theorem

{n : ℕ} {a b : Fin n} : a + b < a ↔ rev b < a

Full source

lemma add_lt_left_iff {n : ℕ} {a b : Fin n} : a + b < a ↔ rev b < a := by
  rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]

Left Addition Inequality Characterization via Reverse in $\mathrm{Fin}(n)$

Informal description

For any natural number $n$ and elements $a, b$ in the finite type $\mathrm{Fin}(n)$, the inequality $a + b < a$ holds if and only if $\mathrm{rev}(b) < a$, where $\mathrm{rev}$ denotes the reverse operation on $\mathrm{Fin}(n)$.