Documentation

Incompleteness.ToFoundation.Basic

@[inline]
def Fin.addCast {n : } (m : ) :
Fin nFin (m + n)
Equations
Instances For
    @[simp]
    theorem Fin.addCast_val {n m : } (i : Fin n) :
    (addCast m i) = i
    @[simp]
    theorem Matrix.appeendr_addCast {α : Type u_1} {m n : } (u : Fin mα) (v : Fin nα) (i : Fin m) :
    appendr u v (Fin.addCast n i) = u i
    @[simp]
    theorem Matrix.appeendr_addNat {α : Type u_1} {m n : } (u : Fin mα) (v : Fin nα) (i : Fin n) :
    appendr u v (i.addNat m) = v i