Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-23 12:40 83ec6e06

View on Github →

feat(analysis/normed_space/inner_product): inner product is infinitely smooth (#5089)

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

added theorem continuous_inner

added theorem differentiable.inner

added theorem differentiable_at.inner

added theorem differentiable_inner

added theorem differentiable_on.inner

added theorem differentiable_within_at.inner

added theorem inner_smul_real_left

added theorem inner_smul_real_right

added theorem is_bounded_bilinear_map_inner

added theorem times_cont_diff.inner

added theorem times_cont_diff_at.inner

added theorem times_cont_diff_at_inner

added theorem times_cont_diff_inner

added theorem times_cont_diff_on.inner

added theorem times_cont_diff_within_at.inner

Modified src/data/complex/is_R_or_C.lean

added theorem is_R_or_C.algebra_map_eq_of_real