Mathlib v3 is deprecated. Go to Mathlib v4

Structure is_add_regular

Modification history

2022-04-05 09:11

src/algebra/regular/basic.lean

feat(algebra/group/to_additive + algebra/regular/basic): add to_additive for `is_regular` (#12930) …

Added is_add_regular View on Github →