Commit 2025-03-06 06:02 83b82840

View on Github →

chore(GroupAction/Pointwise): review API (#22563)

  • Move lemmas assuming IsUnit to the IsUnit namespace.
  • Move IsUnit.smul_bijective to an earlier file.
  • Use weaker typeclass assumptions (e.g., SMul instead of MulAction) here and there.
  • Make more arguments implicit.

Estimated changes

added theorem IsUnit.smul_bijective
modified theorem Group.preimage_smul_set
modified theorem Set.MapsTo.smul_set
modified theorem Set.MapsTo.smul_setₛₗ
modified theorem image_smul_set
modified theorem image_smul_setₛₗ
deleted theorem preimage_smul_set
modified theorem preimage_smul_setₛₗ'
deleted theorem preimage_smul_setₛₗ
deleted theorem smul_preimage_set_le