Commit 2024-03-17 17:51 9d3f2bf8

View on Github →

chore(Algebra): improve argument names to induction principles (#11439) These are the case names used by the induction tactic after the with. This replaces H0, H1, Hmul etc with zero, one, mul. This PR does not touch Submonoid or Subgroup, as to_additive does not know how to rename the argument names. There are ways to work around this, but I'd prefer to leave them to a later PR. This also leaves the closure_induction₂ variants alone, as renaming the arguments is more work for less gain.

Estimated changes