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

theorem Mathlib.Tactic.Group.zpow_trick {G : Type u_1} [Group G] (a b : G) (n m : ℤ) : a * b ^ n * b ^ m = a * b ^ (n + m)

theorem Mathlib.Tactic.Group.zsmul_trick {G : Type u_1} [AddGroup G] (a b : G) (n m : ℤ) : a + n • b + m • b = a + (n + m) • b

theorem Mathlib.Tactic.Group.zpow_trick_one {G : Type u_1} [Group G] (a b : G) (m : ℤ) : a * b * b ^ m = a * b ^ (m + 1)

theorem Mathlib.Tactic.Group.zsmul_trick_zero {G : Type u_1} [AddGroup G] (a b : G) (m : ℤ) : a + b + m • b = a + (m + 1) • b

theorem Mathlib.Tactic.Group.zpow_trick_one' {G : Type u_1} [Group G] (a b : G) (n : ℤ) : a * b ^ n * b = a * b ^ (n + 1)

theorem Mathlib.Tactic.Group.zsmul_trick_zero' {G : Type u_1} [AddGroup G] (a b : G) (n : ℤ) : a + n • b + b = a + (n + 1) • b

def Mathlib.Tactic.Group.aux_group₁ : Lean.ParserDescr

Auxiliary tactic for the group tactic. Calls the simplifier only.

Equations

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

def Mathlib.Tactic.Group.aux_group₂ : Lean.ParserDescr

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.

def Mathlib.Tactic.Group.group : Lean.ParserDescr

group normalizes expressions in multiplicative groups that occur in the goal. group does not assume commutativity, instead using only the group axioms without any information about which group is manipulated. If the goal is an equality, and after normalization the two sides are equal, group closes the goal.

For additive commutative groups, use the abel tactic instead.

• group at l1 l2 ... normalizes at the given locations.

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.

We register group with the hint tactic.