Documentation

Batteries.Data.Fin.Lemmas

clamp #

@[simp]
theorem Fin.coe_clamp (n m : Nat) :
(Fin.clamp n m) = min n m