Commit 2023-02-04 14:04 b933c663

View on Github →

feat: port Data.Holor (#1669)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Holor.lean

added inductive Holor.CPRankMax1

added inductive Holor.CPRankMax

added def Holor.assocLeft

added def Holor.assocRight

added theorem Holor.cast_type

added theorem Holor.cprankMax_1

added theorem Holor.cprankMax_add

added theorem Holor.cprankMax_mul

added theorem Holor.cprankMax_nil

added theorem Holor.cprankMax_sum

added theorem Holor.cprankMax_upper_bound

added theorem Holor.cprank_upper_bound

added theorem Holor.holor_index_cons_decomp

added def Holor.mul

added theorem Holor.mul_assoc0

added theorem Holor.mul_assoc

added theorem Holor.mul_left_distrib

added theorem Holor.mul_right_distrib

added theorem Holor.mul_scalar_mul

added def Holor.slice

added theorem Holor.slice_add

added theorem Holor.slice_eq

added theorem Holor.slice_sum

added theorem Holor.slice_unit_vec_mul

added theorem Holor.slice_zero

added theorem Holor.sum_unit_vec_mul_slice

added def Holor.unitVec

added def Holor

added def HolorIndex.assocLeft

added def HolorIndex.assocRight

added theorem HolorIndex.cast_type

added def HolorIndex.drop

added theorem HolorIndex.drop_drop

added theorem HolorIndex.drop_take

added def HolorIndex.take

added theorem HolorIndex.take_take

added def HolorIndex