Changelog (unreleased)

[Unreleased]

Added

in mathcomp_extra.v:
- lemmas prodr_ile1, nat_int
in normedtype.v:
- lemma scaler1
in derive.v:
- lemmas horner0_ext, hornerD_ext, horner_scale_ext, hornerC_ext, derivable_horner, derivE, continuous_horner
- instance is_derive_poly
in lebesgue_integral.v:
- lemmas integral_fin_num_abs, Rintegral_cst, le_Rintegral
new file pi_irrational.v:
- lemmas measurable_poly
- definition rational
- module pi_irrational
- lemma pi_irrationnal
in numfun.v
- lemmas funeposE, funenegE, funepos_comp, funeneg_comp
in classical_sets.v:
- lemmas xsectionE, ysectionE

Changed

in lebesgue_integrale.v
- change implicits of measurable_funP
in derive.v:
- put the notation ^`() and ^`( _ ) in scope classical_set_scope
in numfun.v
- lock funepos, funeneg
moved from lebesgue_integral.v to measure.v and generalized
- lemmas measurable_xsection, measurable_ysection

Renamed

in measure.v
- preimage_class -> preimage_set_system
- image_class -> image_set_system
- preimage_classes -> g_sigma_preimageU
- preimage_class_measurable_fun -> preimage_set_system_measurable_fun
- sigma_algebra_preimage_class -> sigma_algebra_preimage
- sigma_algebra_image_class -> sigma_algebra_image
- sigma_algebra_preimage_classE -> g_sigma_preimageE
- preimage_classes_comp -> g_sigma_preimageU_comp

Generalized

Deprecated

Removed

Infrastructure

Misc