Commit 2023-03-17 16:27 254ad096

feat: port Algebra.TrivSqZeroExt (#2951) Note that the note on the port comment wiki is out of date; the PR to wait for has made it through mathport already. The main difficulty here comes from the fact that Lean can no longer work out the type of the zero in (r • 0 : M) due to • being HSMul. The rest of the port is just adding instance names, and one cases where cases n resulted in an unwanted Nat.zero where using match n gives a better 0.