Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-10 21:52 dfa73639

View on Github →

feat(analysis/normed_space/finite_dimension): finite-dimensionality of spaces of continuous linear map (#10259)

Estimated changes

Modified src/analysis/inner_product_space/basic.lean

added theorem inner_product_space.of_core.inner_self_eq_norm_mul_norm

deleted theorem inner_product_space.of_core.inner_self_eq_norm_sq

added theorem inner_self_eq_norm_mul_norm

modified theorem inner_self_eq_norm_sq

added theorem real_inner_self_eq_norm_mul_norm

modified theorem real_inner_self_eq_norm_sq

Modified src/analysis/inner_product_space/calculus.lean

Modified src/analysis/inner_product_space/dual.lean

added theorem inner_product_space.to_dual_symm_apply

Modified src/analysis/inner_product_space/rayleigh.lean

Modified src/analysis/normed_space/dual.lean

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/quaternion.lean

Modified src/geometry/euclidean/basic.lean

Modified src/geometry/euclidean/circumcenter.lean

Modified src/geometry/euclidean/triangle.lean

Modified src/geometry/manifold/instances/sphere.lean

Modified src/topology/algebra/module.lean

added def continuous_linear_map.coe_lm