Fin is a group

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

See note [foundational algebra order theory].

Instances

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

Equations

• Fin.addCommSemigroup n = AddCommSemigroup.mk ⋯

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

Equations

• Fin.instAddCommSemigroup n = AddCommSemigroup.mk ⋯

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

Equations

• Fin.addCommMonoid n = let __spread.0 := Fin.addCommSemigroup n; AddCommMonoid.mk ⋯

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

Equations

• Fin.instAddMonoidWithOne n = let __spread.0 := inferInstanceAs (AddCommMonoid (Fin n)); AddMonoidWithOne.mk ⋯ ⋯

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

Equations

• Fin.addCommGroup n = let __spread.0 := Fin.addCommMonoid n; let __spread.1 := Fin.neg n; AddCommGroup.mk ⋯

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 = InvolutiveNeg.mk ⋯

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

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

Equations

• ⋯ = ⋯

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 = let __src := Fin.addCommSemigroup n; let __src_1 := ⋯; AddLeftCancelSemigroup.mk ⋯

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 = let __src := Fin.addCommSemigroup n; let __src_1 := ⋯; AddRightCancelSemigroup.mk ⋯

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_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 : ℕ) : -Fin.last n = 1

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