Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-06 13:54 eeb194dc

View on Github →

feat(analysis/normed_space/inner_product): facts about the span of a single vector, mostly in inner product spaces (#5589)

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

added theorem findim_orthogonal_span_singleton

added theorem inner_left_of_mem_orthogonal_singleton

added theorem inner_right_of_mem_orthogonal_singleton

added theorem orthogonal_projection_bot

added theorem orthogonal_projection_orthogonal_complement_singleton_eq_zero

added theorem orthogonal_projection_singleton

added theorem orthogonal_projection_unit_singleton

added theorem smul_orthogonal_projection_singleton

Modified src/linear_algebra/basic.lean

added theorem submodule.span_zero_singleton

Modified src/linear_algebra/finite_dimensional.lean

added theorem findim_span_singleton