Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-15 16:49 2e752e13

View on Github →

feat(tactic/group): group normalization tactic (#3062) A tactic to normalize expressions in multiplicative groups.

Estimated changes

Modified src/algebra/group_power.lean

added theorem mul_gpow_neg_one

added theorem mul_gpow_self

added theorem mul_self_gpow

Modified src/tactic/default.lean

Created src/tactic/group.lean

added theorem tactic.group.gpow_trick

added theorem tactic.group.gpow_trick_one'

added theorem tactic.group.gpow_trick_one

added theorem tactic.group.gpow_trick_sub

Created test/group.lean

added def commutator3

added def commutator