toCore — Mathlib

Lean4
/-- Define `InnerProductSpace.Core` from `InnerProductSpace`. Defined to reuse lemmas about
`InnerProductSpace.Core` for `InnerProductSpace`s. Note that the `Norm` instance provided by
`InnerProductSpace.Core.norm` is propositionally but not definitionally equal to the original
norm. -/
def toCore [NormedAddCommGroup E] [c : InnerProductSpace 𝕜 E] : InnerProductSpace.Core 𝕜 E :=
  {
    c with
    re_inner_nonneg := fun x => by
      rw [← InnerProductSpace.norm_sq_eq_re_inner]
      apply sq_nonneg
    definite := fun x hx =>
      norm_eq_zero.1 <| pow_eq_zero (n := 2) <| by rw [InnerProductSpace.norm_sq_eq_re_inner (𝕜 := 𝕜) x, hx, map_zero] }
Похожие утверждения