mathlib documentation

algebra.group.default

Various multiplicative and additive structures. #

This file imports all files in this subdirectory except for prod.