group problem

Stream: new members

[BANGJI HU]

import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Defs
import Mathlib

example {G:Type} [Group G] {g:G}:oderOf g=1↔g=1:=by
constructor
intro h
rw[← @orderOf_eq_one_iff]

[BANGJI HU]

why does assumption doesnt work

[Johan Commelin]

Please post a #mwe

[Edward van de Meent]

the answer is that you're misspelling orderOf g as oderOfg

[BANGJI HU]

import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Defs
import Mathlib

example {G:Type} [Group G] {g:G}:oder Of g=1↔g=1:=by
constructor
intro h
rw[← @orderOf_eq_one_iff]

[Edward van de Meent]

you're still misspelling it... note the second r and lack of space in orderOf. here is the fixed version:

import Mathlib.GroupTheory.OrderOfElement

example {G:Type} [Group G] {g:G}: orderOf g=1↔g=1:=by
  constructor
  . intro h
    rw[← orderOf_eq_one_iff]
    assumption
  sorry

[BANGJI HU]

import Mathlib.GroupTheory.OrderOfElement


example {G : Type*} [Group G] {a b c:G} : oderOf (a* b* c)=oderOf (b*c*a) :=by

[BANGJI HU]

expected type?

[Notification Bot]

2 messages were moved here from #new members > group by Johan Commelin.

[Johan Commelin]

@hand bob Please

• Do not post your messages in random threads but start a new appropriate thread
• Write orderOf instead of oderOf. This mistake has been pointed out before
• Give more details about what exactly your question is. Where are you stuck? What have you tried? "expected type?" is not a question.

[BANGJI HU]

what do you mean by start a new appropriate thread,and sorry i am chiness just afresh

[BANGJI HU]

i want to prove that let a be an element of a group G.prove ord(a)=1 iff a=1

[Edward van de Meent]

did this not help?

[BANGJI HU]

import Mathlib.Tactic
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Defs
import Mathlib.GroupTheory.OrderOfElement

example {G:Type} [Group G] {m n:ℕ}{a b :G}: orderOf a=orderOf (b*a*b⁻¹):=by
let n   :=orderOf a
have : aⁿ=1 :=by sorry
have : b*aⁿn*b⁻¹=b*1*b⁻¹ :=by sorry
have : b*aⁿ*b⁻¹=1 :=by sorry
calc (b*a*b⁻¹)ⁿ=b*aⁿ*b⁻¹ :=by sorry
have :orderOf (b*a*b⁻¹)=n :=by sorry

[Daniel Weber]

There's no ⁿ notation - you need to write a ^ n = 1.

[BANGJI HU]

i just want to step by step to proof

[Edward van de Meent]

import Mathlib.Tactic
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Defs
import Mathlib.GroupTheory.OrderOfElement

lemma orderOf_eq_of_Semiconjby {G:Type} [Group G] (a:G) {x y :G} (h : SemiconjBy a x y) :
    orderOf  x = orderOf y := by
  rw [orderOf_eq_orderOf_iff]
  intro n
  have : a * (x ^ n) * a⁻¹ = (y^n) := by calc
    a * x ^ n * a⁻¹
      = (a * x * a⁻¹) ^ n := by rw [conj_pow]
    _ = (y * a * a⁻¹) ^ n := by rw [h.eq]
    _ = y ^ n := by rw [mul_inv_cancel_right]
  rw [← this]
  rw [conj_eq_one_iff]


example {G:Type} [Group G] {m n:ℕ}{a b :G}: orderOf a=orderOf (b*a*b⁻¹):=by
  apply orderOf_eq_of_Semiconjby b
  exact SemiconjBy.conj_mk b a

[Ruben Van de Velde]

With another lemma:

import Mathlib.GroupTheory.OrderOfElement

variable {G:Type*} [Group G] (a:G) {x y :G} (h : SemiconjBy a x y)
lemma SemiconjBy.eq_one_iff : x = 1 ↔ y = 1 := by
  rw [← conj_eq_one_iff (a := a) (b := x), h.eq, mul_inv_cancel_right]
#find_home SemiconjBy.eq_one_iff -- Mathlib.Algebra.Group.Semiconj.Basic

lemma SemiconjBy.orderOf_eq : orderOf x = orderOf y := by
  rw [orderOf_eq_orderOf_iff]
  intro n
  exact (h.pow_right n).eq_one_iff
#find_home! SemiconjBy.orderOf_eq -- Mathlib.GroupTheory.OrderOfElement

example {G:Type} [Group G] {m n:ℕ}{a b :G}: orderOf a=orderOf (b*a*b⁻¹):=
  SemiconjBy.conj_mk b a |>.orderOf_eq

[Ruben Van de Velde]

@Edward van de Meent , do you want to PR those two lemmas to mathlib?

[Ralf Stephan]

(deleted)

[Edward van de Meent]

Ruben Van de Velde said:

Edward van de Meent , do you want to PR those two lemmas to mathlib?

#14674

[Edward van de Meent]

ah, should these lemmas be protected?

[Ruben Van de Velde]

Maybe?

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Eric Wieser]

Edward van de Meent said:

did this not help?

@hand bob, I've merged your repeated questions into a single thread, because I think they're all the same question

[Notification Bot]

hand bob has marked this topic as resolved.

[Notification Bot]

hand bob has marked this topic as unresolved.

[BANGJI HU]

import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Defs
import Mathlib
import Mathlib.Tactic

open Set
open Subgroup MonoidHom
open Subgroup
theorem eqord3 {G : Type*} [Group G] (a b: G)(h:orderOf a  =2 ): (∀ b:G,orderOf (b⁻¹ * a * b)=2)
:=by

[BANGJI HU]

Special cases are more difficult than ordinary ones