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) :
    (Fin.addCast m i) = i
    @[simp]
    theorem Matrix.appeendr_addCast {α : Type u_1} {m : } {n : } (u : Fin mα) (v : Fin nα) (i : Fin m) :
    @[simp]
    theorem Matrix.appeendr_addNat {α : Type u_1} {m : } {n : } (u : Fin mα) (v : Fin nα) (i : Fin n) :
    Matrix.appendr u v (i.addNat m) = v i