Theorem Sym2.lift_smul_lift

Modification history

2025-02-18 20:17
Mathlib/Data/Sym/Sym2.lean
feat(Data/Sym/Sym2): Multiplication as a function from `Sym2` (#21836) …
Added Sym2.lift_smul_liftView on Github →