Commit 2024-01-14 05:39 350879f7

View on Github →

feat: add Inducing.continuousSMul (#9713)

  • add Inducing.continuousSMul and Inducing.continuousVAdd;
  • use it to golf Units.continuousSMul and Inducing.continuousMul;
  • generalize Submonoid.continuousSMul from a submonoid of a group to a submonoid of a monoid;
  • reuse Submonoid.continuousSMul in Subgroup.continuousSMul.

Estimated changes

modified theorem continuousSMul_induced