Theorem 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 star_dotProduct_toMatrix₂_mulVec View on Github →