Commit 2021-03-08 12:32 7058fa61

View on Github →

feat(linear_algebra/{bilinear,quadratic}_form): inherit scalar actions from algebras (#6586) For example, this means a quadratic form over the quaternions inherits an ℝ action.

Estimated changes

Modified src/linear_algebra/bilinear_form.lean

modified theorem bilin_form.smul_apply

Modified src/linear_algebra/quadratic_form.lean

modified theorem quadratic_form.coe_fn_smul

modified theorem quadratic_form.smul_apply