`group` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

theorem tactic.group.zsmul_trick {G : Type u_1} [add_group G] (a b : G) (n m : ℤ) :

a + n • b + m • b = a + (n + m) • b

source

theorem tactic.group.zpow_trick {G : Type u_1} [group G] (a b : G) (n m : ℤ) :

a * b ^ n * b ^ m = a * b ^ (n + m)

source

theorem tactic.group.zpow_trick_one {G : Type u_1} [group G] (a b : G) (m : ℤ) :

a * b * b ^ m = a * b ^ (m + 1)

source

theorem tactic.group.zsmul_trick_zero {G : Type u_1} [add_group G] (a b : G) (m : ℤ) :

a + b + m • b = a + (m + 1) • b

source

theorem tactic.group.zpow_trick_one' {G : Type u_1} [group G] (a b : G) (n : ℤ) :

a * b ^ n * b = a * b ^ (n + 1)

source

theorem tactic.group.zsmul_trick_zero' {G : Type u_1} [add_group G] (a b : G) (n : ℤ) :

a + n • b + b = a + (n + 1) • b

source

theorem tactic.group.zsmul_trick_sub {G : Type u_1} [add_group G] (a b : G) (n m : ℤ) :

a + n • b + -m • b = a + (n - m) • b

source

theorem tactic.group.zpow_trick_sub {G : Type u_1} [group G] (a b : G) (n m : ℤ) :

a * b ^ n * b ^ -m = a * b ^ (n - m)

source

meta def tactic.aux_group₁ (locat : interactive.loc) :

tactic unit

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

source

meta def tactic.aux_group₂ (locat : interactive.loc) :

tactic unit

Auxiliary tactic for the group tactic. Calls ring_nf to normalize exponents.

source

meta def tactic.interactive.group (locat : interactive.parse interactive.types.location) :

tactic unit

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 :=
begin
  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
end

source

def tactic_doc.tactic.group :

tactic_doc_entry

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 :=
begin
  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
end

group #

Tags #

`group` #