Commit 2023-10-23 17:38 55c25193

chore(Algebra/Group/TypeTags): lemmas about pow and smul (#7862) Half of these lemmas already existed, but were a long way from the definition that define the operators. For the ones that did exist, the #aligns have been kept. The new lemmas are all @[simp] since that matches the corresponding add/mul lemmas. This makes some lemmas about Int and Nat not simp-normal any more (they disagree on commutativity), but that doesn't seem to matter.