Commit 2021-11-09 08:19 d4ec6b47

View on Github →

feat(Data/Fin/Basic) (#84) Add some lemmas and instances for Fin. I'm not sure whether this definition of Fin.gsmul is okay. The one in mathlib3 is super buried, so I couldn't figure out how it's actually defined (it' called zsmul in mathlib3).

Estimated changes

added theorem Fin.add_assoc
added theorem Fin.add_comm
added theorem Fin.add_def
added theorem Fin.add_left_neg
added theorem Fin.add_zero
added def Fin.checkedAdd
added def Fin.checkedMul
added def Fin.checkedSub
added theorem Fin.checked_add_spec
added theorem Fin.checked_mul_spec
added theorem Fin.checked_sub_spec
added def Fin.gsmul
added theorem Fin.gsmul_neg'
added theorem Fin.gsmul_succ'
added theorem Fin.gsmul_zero'
added theorem Fin.mod_eq
added theorem Fin.modn_def
added theorem Fin.mul_comm
added theorem Fin.mul_def
added def Fin.nsmul
added theorem Fin.nsmul_succ'
added theorem Fin.nsmuls_eq
added theorem Fin.of_nat_zero
added theorem Fin.positive_size
added theorem Fin.sub_def
added theorem Fin.sub_eq_add_neg
added theorem Fin.val_one
added theorem Fin.val_zero
added theorem Fin.zero_add
added theorem Fin.zero_mul
added theorem Nat.add_mod
added theorem Nat.add_mod_mod
added theorem Nat.mod_add_mod
added theorem Nat.mod_mod
added theorem Nat.mul_mod