To avoid having old PRs put changes into the wrong section of the CHANGELOG, new entries now go to the present file as discussed here.
The format is based on Keep a Changelog.
-
in
seq.v
- lemmas
subset_mapP
,take_min
,take_taker
,perm_allpairs_dep
,perm_allpairs
- lemmas
-
in
path.v
- lemmas
prefix_path
,prefix_sorted
,infix_sorted
,suffix_sorted
- lemmas
-
in
ssralg.v
- lemmas
natr1
,nat1r
,telescope_sumr_eq
,telescope_prodr_eq
,telescope_prodf_eq
- lemmas
-
in
poly.v
- definitions
even_poly
,odd_poly
,take_poly
,drop_poly
- lemmas
comm_polyD
,comm_polyM
,comm_poly_exp
,root_exp
,root_ZXsubC
,size_mulXn
,coef_sumMXn
,comp_Xn_poly
,coef_comp_poly_Xn
,comp_poly_Xn
,size_even_poly
,size_even_poly_eq
,coef_even_poly
,even_polyE
,even_polyD
,even_polyZ
,even_poly_is_linear
,even_polyC
,size_odd_poly
,coef_odd_poly
,odd_polyE
,odd_polyC
,odd_polyD
,odd_polyZ
,odd_poly_is_linear
,odd_polyMX
,even_polyMX
,sum_even_poly
,sum_odd_poly
,poly_even_odd
,size_take_poly
,coef_take_poly
,take_poly_id
,take_polyD
,take_polyZ
,take_poly_is_linear
,take_poly_sum
,take_poly0l
,take_poly0r
,take_polyMXn
,take_polyMXn_0
,take_polyDMXn
,size_drop_poly
,size_drop_poly_eq
,coef_drop_poly
,drop_poly_eq0
,sum_drop_poly
,drop_polyD
,drop_polyZ
,drop_poly_is_linear
,drop_poly_sum
,drop_poly0l
,drop_poly0r
,drop_polyMXn
,drop_polyMXn_id
,drop_polyDMXn
,poly_take_drop
,eqp_take_drop
,scale_polyC
- canonical instances
even_poly_additive
,even_poly_linear
,odd_poly_additive
,odd_poly_linear
,take_poly_additive
,take_poly_linear
,drop_poly_additive
,drop_poly_linear
- definitions
-
in
polydiv.v
- lemmas
Pdiv.RingMonic.drop_poly_rdivp
,Pdiv.RingMonic.take_poly_rmodp
,Pdiv.IdomainMonic.drop_poly_divp
,Pdiv.IdomainMonic.take_poly_modp
- lemmas
-
in
bigop.v
- lemmas
big_ord1_eq
,big_ord1_cond_eq
,big_nat1_eq
,big_nat1_cond_eq
- lemmas
-
in
eqtype.v
- lemmas
existsb
andexists_inb
- lemmas
-
in
seq.v
- lemma
if_nth
- lemma
-
in
ssrbool.v
- lemmas
if_and
,if_or
,if_implyb
,if_impliybC
,if_add
- lemmas
-
in
ssralg.v
- lemma
eqr_sum_div
- lemma
-
in
ssrnum.v
- lemmas
psumr_neq0
,psumr_neq0P
- lemmas
-
in
ssrnat.v
- lemma
leqVgt
- lemmas
ltn_half_double
,leq_half_double
,gtn_half_double
- lemma
double_pred
- lemmas
uphalfE
,ltn_uphalf_double
,geq_uphalf_double
,gtn_uphalf_double
- lemmas
halfK
,uphalfK
,odd_halfK
,even_halfK
,odd_uphalfK
,even_uphalfK
- lemmas
leq_sub2rE
,leq_sub2lE
,ltn_sub2rE
,ltn_sub2lE
- lemma
-
in
ssrint.v
- printing only notation for
x = y :> int
, openingint_scope
onx
andy
to better match the already existing parsing only notation with the introduction of number notations inring_scope
- printing only notation for
-
in
bigop.v
- lemmas
big_seq1_id
,big_nat1_id
,big_pred1_eq_id
,big_pred1_id
,big_const_idem
,big1_idem
,big_id_idem
,big_rem_AC
,perm_big_AC
,big_enum_cond_AC
,bigD1_AC
,bigD1_seq_AC
,big_image_cond_AC
,big_image_AC
,big_image_cond_id_AC
,Lemma
,cardD1x
,reindex_omap_AC
,reindex_onto_AC
,reindex_AC
,reindex_inj_AC
,bigD1_ord_AC
,big_enum_val_cond_AC
,big_enum_rank_cond_AC
,big_nat_rev_AC
,big_rev_mkord_AC
,big_mkcond_idem
,big_mkcondr_idem
,big_mkcondl_idem
,big_rmcond_idem
,big_rmcond_in_idem
,big_cat_idem
,big_allpairs_dep_idem
,big_allpairs_idem
,big_cat_nat_idem
,big_split_idem
,big_id_idem_AC
,bigID_idem
,bigU_idem
,partition_big_idem
,sig_big_dep_idem
,pair_big_dep_idem
,pair_big_idem
,pair_bigA_idem
,exchange_big_dep_idem
,exchange_big_idem
,exchange_big_dep_nat_idem
,exchange_big_nat_idem
,big_undup_AC
- lemmas
-
in
matrix.v
- definitions
Vandrmonde
,map2_mx
- lemma
det_Vandermonde
,map2_trmx
,map2_const_mx
,map2_row
,map2_col
,map2_row'
,map2_col'
,map2_mxsub
,map2_row_perm
,map2_col_perm
,map2_xrow
,map2_xcol
,map2_castmx
,map2_conform_mx
,map2_mxvec
,map2_vec_mx
,map2_row_mx
,map2_col_mx
,map2_block_mx
,map2_lsubmx
,map2_rsubmx
,map2_usubmx
,map2_dsubmx
,map2_ulsubmx
,map2_ursubmx
,map2_dlsubmx
,map2_drsubmx
,eq_in_map2_mx
,eq_map2_mx
,map2_mx_left_in
,map2_mx_left
,map2_mx_right_in
,map2_mx_right
,map2_mxA
,map2_1mx
,map2_mx1
,map2_mxC
,map2_0mx
,map2_mx0
,map2_mxDl
,map2_mxDr
,diag_mx_is_additive
,mxtrace_is_additive
- definitions
-
in
ssralg.v
- lemmas
divrN
,divrNN
- lemmas
-
in
poly.v
:- generalize
eq_poly
- generalize
-
in
poly.v
:- made hornerE preserve powers
-
in
matrix.v
:- updated
oppmx
,addmx
,addmxA
,addmxC
,add0mx
- moved to an earlier section of the file
diag_mx
,tr_diag_mx
,diag_mx_row
,diag_mxP
,diag_mx_is_diag
,diag_mx_is_trig
,scalar_mx
,diag_const_mx
,tr_scalar_mx
,scalar_mx_is_additive
,is_scalar_mx
,is_scalar_mxP
,scalar_mx_is_scalar
,mx0_is_scalar
,scalar_mx_is_diag
,is_scalar_mx_is_diag
,scalar_mx_is_trig
,is_scalar_mx_is_trig
,mx11_scalar
,scalar_mx_block
,mxtrace
,mxtrace_tr
,mxtrace0
,mxtraceD
,mxtrace_diag
,mxtrace_scalar
,trace_mx11
,mxtrace_block
- updated
-
in
matrix.v
:- notation
card_matrix
(deprecated in 1.13.0)
- notation
-
in
rat.v
:- notation
divq_eq
(deprecated in 1.13.0)
- notation
-
in
ssralg.v
:- notation
prodr_natmul
(deprecated in 1.13.0)
- notation
-
in
bigop.v
:- notation
big_uncond
(deprecated in 1.13.0)
- notation
-
in
finset.v
:- notations
mem_imset_eq
andmem_imset2_eq
(deprecated in 1.13.0)
- notations
-
in
order.v
:- notations
join_sup_seq
,join_min_seq
,join_sup
,join_min
,join_seq
,meet_inf_seq
,meet_max_seq
,meet_seq
(deprecated in 1.13.0)
- notations
-
in
path.v
:- notations
sup_path_in
,sub_cycle_in
,sub_sorted_in
,eq_path_in
,eq_cycle_in
(deprecated in 1.13.0)
- notations
-
in
seq.v
:- notation
iota_add
(deprecated in 1.13.0)
- notation
-
in
ssreflect.v
:- module
Deprecation
(deprecated in 1.13.0) - notatin
deprecate
(deprecated in 1.13.0)
- module
-
in
ssrnat.v
:- notatin
fact_smonotone
(deprecated in 1.13.0)
- notatin