Documentation

Std.Data.Fin.Init.Lemmas

source
@[simp]
theorem Fin.zero_eta {n : Nat} :
{ val := 0, isLt := (_ : 0 < Nat.succ n) } = 0