Mathlib v3 is deprecated. Go to Mathlib v4

Theorem skew_adjoint.smul_mem

Modification history

2022-02-18 14:37
src/algebra/star/self_adjoint.lean
chore(algebra/star/self_adjoint): extract a lemma from `has_scalar` (#12121)
Added skew_adjoint.smul_memView on Github →