Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-08 18:18 4c9499fc

View on Github →

chore(algebra/group/pi): Split into multiple files (#5280) This allows files that appear before ordered_group to still use pi.monoid etc.

Estimated changes

deleted theorem pi.div_apply
deleted theorem pi.inv_apply
deleted theorem pi.mul_apply
deleted theorem pi.one_apply
added theorem pi.div_apply
added theorem pi.inv_apply
added theorem pi.mul_apply
added theorem pi.one_apply