Commit 2019-08-08 02:35 9c4dd950

feat (analysis/normed_space): Define real inner product space (#1248)

• Inner product space
• Change the definition of inner_product_space The original definition introduces an instance loop. See Zulip talks: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/ring.20tactic.20works.20at.20one.20place.2C.20fails.20at.20another
• Orthogonal Projection Prove the existence of orthogonal projections onto complete subspaces in an inner product space.
• Fix names
• small fixes