Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-18 14:37 223f1496

View on Github →

chore(algebra/star/self_adjoint): extract a lemma from has_scalar (#12121)

Estimated changes

added theorem self_adjoint.smul_mem
added theorem skew_adjoint.smul_mem