Theorem Units.smul_mk_apply

Modification history

2024-07-04 21:34

Mathlib/Algebra/Group/Action/Units.lean

chore: Move `MulAction` on `Opposite`, `Pi`, `Prod`, `Sum`, `Sigma`, `Units` (#13161) …

Modified Units.smul_mk_apply View on Github →

2024-02-19 15:34

Mathlib/GroupTheory/GroupAction/Units.lean

feat(LinearAlgebra/Matrix): center of special linear group (#7826) …

Added Units.smul_mk_apply View on Github →