mathlib3
619c1b0d - chore({algebra, algebraic_geometry}/*): move 1 module doc and split lines (#6294)

Commit
4 years ago
chore({algebra, algebraic_geometry}/*): move 1 module doc and split lines (#6294) This moves the module doc for `algebra/ordered_group` so that it gets recognised by the linter. Furthermore, several lines are split in the algebra and algebraic_geometry folder.
Parents
Loading