Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-01 14:51 7c361fa0

View on Github →

feat(data/holor): holor library

Estimated changes

Created data/holor.lean

added def holor.assoc_left

added def holor.assoc_right

added theorem holor.cast_type

added inductive holor.cprank_max1

added inductive holor.cprank_max

added theorem holor.cprank_max_1

added theorem holor.cprank_max_add

added theorem holor.cprank_max_mul

added theorem holor.cprank_max_nil

added theorem holor.cprank_max_sum

added theorem holor.cprank_max_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 theorem holor.mul_zero

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.unit_vec

added theorem holor.zero_mul

added def holor

added def holor_index.assoc_left

added def holor_index.assoc_right

added theorem holor_index.cast_type

added def holor_index.drop

added theorem holor_index.drop_drop

added theorem holor_index.drop_take

added def holor_index.take

added theorem holor_index.take_take

added def holor_index

Modified data/list/basic.lean

added theorem list.drop_drop

added theorem list.drop_take

added theorem list.forall₂_drop

added theorem list.forall₂_drop_append

added theorem list.forall₂_take

added theorem list.forall₂_take_append