Theorem apply_eq_star_dotProduct_toMatrix₂_mulVec

Modification history

2025-10-23 14:48
Mathlib/LinearAlgebra/SesquilinearForm/Star.lean
feat: properties of sesquilinear forms over a star ring (#30274)
Added apply_eq_star_dotProduct_toMatrix₂_mulVecView on Github →