Theorems · Theorem · global analysis

OrthonormalBasis.fromOrthogonalSpanSingleton.congr_simp

∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (n : ℕ) [inst_3 : Fact (Module.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0),
  OrthonormalBasis.fromOrthogonalSpanSingleton n hv = OrthonormalBasis.fromOrthogonalSpanSingleton n hv

Defined in

Mathlib.Geometry.Manifold.Instances.Sphere

Cited by

0 results in Mathlib

Foundations

Depth 242 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFact