Commit 2025-10-23 14:48 7baeab84

View on Github →

feat: properties of sesquilinear forms over a star ring (#30274)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/SesquilinearForm/Star.lean

added theorem LinearMap.isPosSemidef_iff_posSemidef_toMatrix

added theorem LinearMap.isSymm_iff_basis

added theorem LinearMap.isSymm_iff_isHermitian_toMatrix

added theorem apply_eq_star_dotProduct_toMatrix₂_mulVec

added theorem star_dotProduct_toMatrix₂_mulVec

Modified Mathlib/Tactic/Linter/DirectoryDependency.lean