Commit 2025-03-05 10:07 fbaadf20

View on Github →

chore: move SMulWithZero with SMulZeroClass (#13027) Move the basic content of GroupTheory.GroupAction to new folders Algebra.Group.Action and Algebra.GroupWithZero.Action depending on whether it is additivisable or not.

Estimated changes

added theorem Pi.single_apply_smul
added theorem boole_smul
added theorem ite_zero_smul
added theorem left_ne_zero_of_smul
added theorem smul_eq_zero_of_left
added theorem smul_inv₀
added theorem zero_smul
deleted theorem Pi.single_apply_smul
deleted theorem boole_smul
deleted theorem ite_zero_smul
deleted theorem left_ne_zero_of_smul
deleted theorem smul_eq_zero_of_left
deleted theorem smul_inv₀
deleted theorem zero_smul