Documentation

Std.Data.Fin.Lemmas

@[simp]
theorem Fin.ofNat'_zero_val :
∀ {a : Nat} {h : a > 0}, (Fin.ofNat' 0 h).val = 0
@[simp]
theorem Fin.mod_val {n : Nat} (a : Fin n) (b : Fin n) :
(a % b).val = a.val % b.val
@[simp]
theorem Fin.div_val {n : Nat} (a : Fin n) (b : Fin n) :
(a / b).val = a.val / b.val
@[simp]
theorem Fin.modn_val {n : Nat} (a : Fin n) (b : Nat) :
(Fin.modn a b).val = a.val % b
@[simp]
theorem USize.lt_def {a : USize} {b : USize} :
@[simp]
theorem USize.le_def {a : USize} {b : USize} :
@[simp]
@[simp]
@[simp]
theorem USize.mod_lt (a : USize) (b : USize) (h : 0 < b) :
a % b < b
theorem USize.toNat.inj {a : USize} {b : USize} :