Inner product space on Hᵐᵒᵖ

This file defines the inner product space structure on Hᵐᵒᵖ where we define the inner product naturally. We also define OrthonormalBasis.mulOpposite.

instance MulOpposite.instInner {𝕜 : Type u_1} {H : Type u_2} [Inner 𝕜 H] : Inner 𝕜 Hᵐᵒᵖ

The inner product of Hᵐᵒᵖ is given by ⟪x, y⟫ ↦ ⟪x.unop, y.unop⟫.

@[simp]

theorem MulOpposite.inner_unop {𝕜 : Type u_1} {H : Type u_2} [Inner 𝕜 H] (x y : Hᵐᵒᵖ) : inner 𝕜 (unop x) (unop y) = inner 𝕜 x y

@[simp]

theorem MulOpposite.inner_op {𝕜 : Type u_1} {H : Type u_2} [Inner 𝕜 H] (x y : H) : inner 𝕜 (op x) (op y) = inner 𝕜 x y

instance MulOpposite.instInnerProductSpace {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup H] [InnerProductSpace 𝕜 H] : InnerProductSpace 𝕜 Hᵐᵒᵖ

theorem Module.Basis.mulOpposite_is_orthonormal_iff {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_3} (b : Basis ι 𝕜 H) : Orthonormal 𝕜 ⇑b.mulOpposite ↔ Orthonormal 𝕜 ⇑b

noncomputable def OrthonormalBasis.mulOpposite {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_3} {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι] (b : OrthonormalBasis ι 𝕜 H) : OrthonormalBasis ι 𝕜 Hᵐᵒᵖ

The multiplicative opposite of an orthonormal basis b, i.e., b i ↦ op (b i).

@[simp]

theorem OrthonormalBasis.toBasis_mulOpposite {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_3} {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι] (b : OrthonormalBasis ι 𝕜 H) : b.mulOpposite.toBasis = b.toBasis.mulOpposite