Research proof index

Map a dual pair under a linear equivalence. -/ @[simps] def map (p : DualPair E) (L : E ≃L[ℝ] E') : DualPair E' := ⟨p.π ∘L ↑L.symm, L p.v, (congr_arg p.π <| L.symm_apply_apply p.v).trans p.pairing⟩ theorem update_comp_left (p : DualPair E) (ψ' : F →L[ℝ] G) (φ : E →L[ℝ] F) (w : F) : p.update (ψ' ∘L φ) (ψ' w) = ψ' ∘L p.update φ w := by ext1 u simp only [upd...