group
Normalizes expressions in the language of groups. The basic idea is to use the simplifier
to put everything into a product of group powers (gpow 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
Auxilliary tactic for the group tactic. Calls the simplifier only.
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: