`group`

tactic #

Normalizes expressions in the language of groups. The basic idea is to use the simplifier
to put everything into a product of group powers (`zpow`

which takes a group element and an
integer), then simplify the exponents using the `ring`

tactic. The process needs to be repeated
since `ring`

can normalize an exponent to zero, leading to a factor that can be removed
before collecting exponents again. The simplifier step also uses some extra lemmas to avoid
some `ring`

invocations.

## Tags #

group_theory

Auxiliary tactic for the `group`

tactic. Calls the simplifier only.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Auxiliary tactic for the `group`

tactic. Calls `ring_nf`

to normalize exponents.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Tactic for normalizing expressions in multiplicative groups, without assuming commutativity, using only the group axioms without any information about which group is manipulated.

(For additive commutative groups, use the `abel`

tactic instead.)

Example:

```
example {G : Type} [Group G] (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a := by
group at h -- normalizes `h` which becomes `h : c = d`
rw [h] -- the goal is now `a*d*d⁻¹ = a`
group -- which then normalized and closed
```

## Equations

- One or more equations did not get rendered due to their size.