Fin is a group

This file contains the additive and multiplicative monoid instances on Fin n.

See note [foundational algebra order theory].

Instances

@[implicit_reducible]

instance Fin.addCommSemigroup (n : ℕ) : AddCommSemigroup (Fin n)

Equations

• Fin.addCommSemigroup n = { toAdd := Fin.instAdd, add_assoc := ⋯, add_comm := ⋯ }

@[implicit_reducible]

instance Fin.addCommMonoid (n : ℕ) [NeZero n] : AddCommMonoid (Fin n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def Fin.instAddMonoidWithOne (n : ℕ) [NeZero n] : AddMonoidWithOne (Fin n)

This is not a global instance, but can introduced locally using open Fin.NatCast in ....

This is not an instance because the binop% elaborator assumes that there are no non-trivial coercion loops, but this instance would introduce a coercion from Nat to Fin n and back. Non-trivial loops lead to undesirable and counterintuitive elaboration behavior.

For example, for x : Fin k and n : Nat, it causes x < n to be elaborated as x < ↑n rather than ↑x < n, silently introducing wraparound arithmetic.

Equations

• Fin.instAddMonoidWithOne n = { natCast := fun (i : ℕ) => Fin.ofNat n i, toAddMonoid := inferInstance.toAddMonoid, toOne := One.ofOfNat1, natCast_zero := ⋯, natCast_succ := ⋯ }

@[implicit_reducible]

instance Fin.addCommGroup (n : ℕ) [NeZero n] : AddCommGroup (Fin n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Fin.instInvolutiveNeg (n : ℕ) : InvolutiveNeg (Fin n)

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

Equations

• Fin.instInvolutiveNeg n = { toNeg := Fin.neg n, neg_neg := ⋯ }

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

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

@[implicit_reducible]

instance Fin.instAddLeftCancelSemigroup (n : ℕ) : AddLeftCancelSemigroup (Fin n)

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

Equations

• Fin.instAddLeftCancelSemigroup n = { toAddSemigroup := (Fin.addCommSemigroup n).toAddSemigroup, toIsLeftCancelAdd := ⋯ }

@[implicit_reducible]

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

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

Equations

• Fin.instAddRightCancelSemigroup n = { toAddSemigroup := (Fin.addCommSemigroup n).toAddSemigroup, toIsRightCancelAdd := ⋯ }

Miscellaneous lemmas

theorem Fin.intCast_def' {n : ℕ} [NeZero n] (x : ℤ) : ↑x = if 0 ≤ x then ↑x.natAbs else -↑x.natAbs

Variant of Fin.intCast_def with Nat.cast on the RHS.

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 b : Fin n} : a < a - b ↔ a < b

@[simp]

theorem Fin.sub_le_iff {n : ℕ} {a 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 : ℕ) : -last n = 1

theorem Fin.neg_natCast_eq_one (n : ℕ) : -↑n = 1

theorem Fin.rev_add {n : ℕ} (a b : Fin n) : (a + b).rev = a.rev - b

theorem Fin.rev_sub {n : ℕ} (a b : Fin n) : (a - b).rev = a.rev + b

theorem Fin.lt_add_one_of_succ_lt {n : ℕ} [NeZero n] {a : Fin n} (ha : ↑a + 1 < n) : a < a + 1

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