Documentation

Init.Grind.CommRing.Fin

source
def Lean.Grind.Fin.npow {n : Nat} [NeZero n] (x : Fin n) (y : Nat) :
Fin n
Equations
Instances For
    source
    instance Lean.Grind.Fin.instHPowFinNatOfNeZero {n : Nat} [NeZero n] :
    HPow (Fin n) Nat (Fin n)
    Equations
    source
    @[simp]
    theorem Lean.Grind.Fin.pow_zero {n : Nat} [NeZero n] (a : Fin n) :
    a ^ 0 = 1
    source
    @[simp]
    theorem Lean.Grind.Fin.pow_succ {n : Nat} [NeZero n] (a : Fin n) (n✝ : Nat) :
    a ^ (n✝ + 1) = a ^ n✝ * a
    source
    theorem Lean.Grind.Fin.add_assoc {n : Nat} (a b c : Fin n) :
    a + b + c = a + (b + c)
    source
    theorem Lean.Grind.Fin.add_comm {n : Nat} (a b : Fin n) :
    a + b = b + a
    source
    theorem Lean.Grind.Fin.add_zero {n : Nat} [NeZero n] (a : Fin n) :
    a + 0 = a
    source
    theorem Lean.Grind.Fin.neg_add_cancel {n : Nat} [NeZero n] (a : Fin n) :
    -a + a = 0
    source
    theorem Lean.Grind.Fin.mul_assoc {n : Nat} (a b c : Fin n) :
    a * b * c = a * (b * c)
    source
    theorem Lean.Grind.Fin.mul_comm {n : Nat} (a b : Fin n) :
    a * b = b * a
    source
    theorem Lean.Grind.Fin.zero_mul {n : Nat} [NeZero n] (a : Fin n) :
    0 * a = 0
    source
    theorem Lean.Grind.Fin.mul_one {n : Nat} [NeZero n] (a : Fin n) :
    a * 1 = a
    source
    theorem Lean.Grind.Fin.left_distrib {n : Nat} (a b c : Fin n) :
    a * (b + c) = a * b + a * c
    source
    theorem Lean.Grind.Fin.ofNat_succ {n : Nat} [NeZero n] (a : Nat) :
    OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
    source
    theorem Lean.Grind.Fin.sub_eq_add_neg {n : Nat} [NeZero n] (a b : Fin n) :
    a - b = a + -b
    source
    theorem Lean.Grind.Fin.intCast_neg {n : Nat} [NeZero n] (i : Int) :
    ↑(-i) = -↑i
    source
    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.
    source
    instance Lean.Grind.Fin.instIsCharPFin (n : Nat) [NeZero n] :
    IsCharP (Fin n) n