Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-25 06:48 51ad06e5

View on Github →

refactor(analysis/inner_product_space/*): split big file (#9382) This PR makes a new folder analysis/inner_product_space/* comprising several files splitting the old analysis/normed_space/inner_product (which had reached 2900 lines!). https://leanprover.zulipchat.com/#narrow/stream/116395-maths

Estimated changes

deleted theorem coe_orthonormal_basis
deleted theorem continuous.inner
deleted theorem continuous_at.inner
deleted theorem continuous_inner
deleted theorem continuous_on.inner
deleted theorem deriv_inner_apply
deleted theorem differentiable.dist
deleted theorem differentiable.inner
deleted theorem differentiable.norm
deleted theorem differentiable.norm_sq
deleted theorem differentiable_at.dist
deleted theorem differentiable_at.inner
deleted theorem differentiable_at.norm
deleted theorem differentiable_at.norm_sq
deleted theorem differentiable_inner
deleted theorem differentiable_on.dist
deleted theorem differentiable_on.inner
deleted theorem differentiable_on.norm
deleted theorem differentiable_on.norm_sq
deleted theorem fderiv_inner_apply
deleted def fderiv_inner_clm
deleted theorem fderiv_inner_clm_apply
deleted theorem filter.tendsto.inner
deleted theorem has_deriv_at.inner
deleted theorem has_deriv_within_at.inner
deleted theorem has_fderiv_at.inner
deleted theorem orthogonal_projection_bot
deleted def orthonormal_basis
deleted def reflection
deleted theorem reflection_apply
deleted theorem reflection_bot
deleted theorem reflection_eq_self_iff
deleted theorem reflection_involutive
deleted theorem reflection_map
deleted theorem reflection_map_apply
deleted theorem reflection_reflection
deleted theorem reflection_symm
deleted theorem times_cont_diff.dist
deleted theorem times_cont_diff.inner
deleted theorem times_cont_diff.norm
deleted theorem times_cont_diff.norm_sq
deleted theorem times_cont_diff_at.dist
deleted theorem times_cont_diff_at.inner
deleted theorem times_cont_diff_at.norm
deleted theorem times_cont_diff_at_inner
deleted theorem times_cont_diff_at_norm
deleted theorem times_cont_diff_inner
deleted theorem times_cont_diff_norm_sq
deleted theorem times_cont_diff_on.dist
deleted theorem times_cont_diff_on.inner
deleted theorem times_cont_diff_on.norm
added theorem continuous.inner
added theorem continuous_at.inner
added theorem continuous_inner
added theorem continuous_on.inner
added theorem deriv_inner_apply
added theorem differentiable.dist
added theorem differentiable.inner
added theorem differentiable.norm
added theorem differentiable.norm_sq
added theorem differentiable_at.dist
added theorem differentiable_at.norm
added theorem differentiable_inner
added theorem differentiable_on.dist
added theorem differentiable_on.norm
added theorem fderiv_inner_apply
added def fderiv_inner_clm
added theorem fderiv_inner_clm_apply
added theorem filter.tendsto.inner
added theorem has_deriv_at.inner
added theorem has_fderiv_at.inner
added theorem times_cont_diff.dist
added theorem times_cont_diff.inner
added theorem times_cont_diff.norm
added theorem times_cont_diff_inner
added theorem coe_orthonormal_basis
added def reflection
added theorem reflection_apply
added theorem reflection_bot
added theorem reflection_eq_self_iff
added theorem reflection_involutive
added theorem reflection_map
added theorem reflection_map_apply
added theorem reflection_reflection
added theorem reflection_symm