def Lean.Grind.Fin.npow {n : Nat} [NeZero n] (x : Fin n) (y : Nat) : Fin n

Equations

• Lean.Grind.Fin.npow x y = npowRec y x

instance Lean.Grind.Fin.instHPowFinNatOfNeZero {n : Nat} [NeZero n] : HPow (Fin n) Nat (Fin n)

Equations

• Lean.Grind.Fin.instHPowFinNatOfNeZero = { hPow := Lean.Grind.Fin.npow }

instance Lean.Grind.Fin.instPowFinNatOfNeZero {n : Nat} [NeZero n] : Pow (Fin n) Nat

Equations

• Lean.Grind.Fin.instPowFinNatOfNeZero = { pow := Lean.Grind.Fin.npow }

@[simp]

theorem Lean.Grind.Fin.pow_zero {n : Nat} [NeZero n] (a : Fin n) : a ^ 0 = 1

@[simp]

theorem Lean.Grind.Fin.pow_succ {n : Nat} [NeZero n] (a : Fin n) (n✝ : Nat) : a ^ (n✝ + 1) = a ^ n✝ * a

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 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.instPowFinCoOfNatIntCast {n : Nat} [i : NeZero n] : ToInt.Pow (Fin n) (IntInterval.co 0 ↑n)