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.

              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 : ℕ) :
                  -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