theorem Lean.Grind.Fin.add_assoc {n : Nat} (a b c : Fin n) : a + b + c = a + (b + c)

theorem Lean.Grind.Fin.add_comm {n : Nat} (a b : Fin n) : a + b = b + a

theorem Lean.Grind.Fin.add_zero {n : Nat} [NeZero n] (a : Fin n) : a + 0 = a

theorem Lean.Grind.Fin.neg_add_cancel {n : Nat} [NeZero n] (a : Fin n) : -a + a = 0

theorem Lean.Grind.Fin.mul_assoc {n : Nat} (a b c : Fin n) : a * b * c = a * (b * c)

theorem Lean.Grind.Fin.mul_comm {n : Nat} (a b : Fin n) : a * b = b * a

theorem Lean.Grind.Fin.zero_mul {n : Nat} [NeZero n] (a : Fin n) : 0 * a = 0

theorem Lean.Grind.Fin.mul_one {n : Nat} [NeZero n] (a : Fin n) : a * 1 = a

theorem Lean.Grind.Fin.left_distrib {n : Nat} (a b c : Fin n) : a * (b + c) = a * b + a * c

theorem Lean.Grind.Fin.ofNat_succ {n : Nat} [NeZero n] (a : Nat) : OfNat.ofNat (a + 1) = OfNat.ofNat a + 1

theorem Lean.Grind.Fin.sub_eq_add_neg {n : Nat} [NeZero n] (a b : Fin n) : a - b = a + -b

theorem Nat.sub_sub_right (a : Nat) {b c : Nat} (h : c ≤ b) : a - (b - c) = a + c - b

theorem Lean.Grind.Fin.neg_mul {n : Nat} [NeZero n] (a b : Fin n) : -a * b = -(a * b)

theorem Lean.Grind.Fin.intCast_neg {n : Nat} [NeZero n] (i : Int) : ↑(-i) = -↑i

@[instance_reducible]

instance Lean.Grind.Fin.instCommRingFinOfNeZeroNat (n : Nat) [NeZero n] : CommRing (Fin n)

Equations

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

instance Lean.Grind.Fin.instIsCharPFin (n : Nat) [NeZero n] : IsCharP (Fin n) n

instance Lean.Grind.Fin.instPowIdentityFinOfNatNat : PowIdentity (Fin 2) 2