Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 06:26 a252427a

View on Github →

chore(algebra/algebra/basic): fix instances names to make doc links work (#10834) The blank lines avoid sentences being pulled into the bulleted list above them.

Estimated changes