Commit 2024-10-23 02:08 ebbced44

chore(Algebra): re-add @[simp] attributes lost in the port (#18057) This PR re-adds the @[simp] attributes that had a porting note that they could be proved by @[simp], but where that does not appear to be the case currently. Of course, the simp set may have changed sufficiently to require un@[simp]ing some of these anyway, but we should add a more up to date comment in that case.