Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-31 10:35 7833dbe4

View on Github →

lint(algebra/*): fix some lint errors (#13058)

  • add some docstrings to additive versions;
  • make with_zero.ordered_add_comm_monoid reducible.

Estimated changes

modified theorem mul_equiv.apply_symm_apply
modified theorem mul_equiv.symm_apply_apply