Commit 2025-02-18 20:17 ea0f577d

View on Github →

feat(Data/Sym/Sym2): Multiplication as a function from Sym2 (#21836) Used in #18578

Estimated changes

added theorem Sym2.lift_smul_lift
added def Sym2.mul
added theorem Sym2.mul_mk