[Merged by Bors] - feat(analysis/normed_space/inner_product): existence of orthonormal basis

docs/undergrad.yaml

@@ -217,7 +217,7 @@ Bilinear and Quadratic Forms Over a Vector Space:
     orthogonal complement: 'submodule.orthogonal'
     Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
     norm: 'inner_product_space.of_core.to_has_norm'
-    orthonormal bases:
+    orthonormal bases: 'maximal_orthonormal_iff_is_basis_of_finite_dimensional'
   Endomorphisms:
     orthogonal group:
     unitary group:
@@ -432,7 +432,7 @@ Topology:
     dual space: 'normed_space.dual.inst'
     Riesz representation theorem: 'inner_product_space.to_dual'
     $l^2$ and $L^2$ cases:
-    Hilbert (orthonormal) bases (in the separable case):
+    Hilbert (orthonormal) bases (in the separable case): 'exists_is_orthonormal_dense_span'
     Hilbert basis of trigonometric polynomials:
     Hilbert bases of orthogonal polynomials:
     Lax-Milgram theorem:

src/algebra/group_power/basic.lean

@@ -624,6 +624,18 @@ pow_bit0_pos h 1
 
 end linear_ordered_ring
 
+@[simp] lemma eq_of_pow_two_eq_pow_two [linear_ordered_comm_ring R]
+  {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) :
+  a ^ 2 = b ^ 2 ↔ a = b :=
+begin
+  refine ⟨_, congr_arg _⟩,
+  intros h,
+  refine (eq_or_eq_neg_of_pow_two_eq_pow_two _ _ h).elim id _,
+  rintros rfl,
+  rw le_antisymm (neg_nonneg.mp ha) hb,
+  exact neg_zero
+end
+
 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
 by simp [pow, monoid.pow]