Commutativity of div_eq_mul_inv

Stream: new members

[Shadman Sakib]

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric

lemma mul_inv_eq_div {G : Type} [_inst_1 : div_inv_monoid G] (a b : G) : b⁻¹ * a = a / b :=
begin
  sorry,
end

[Shadman Sakib]

How would I show that a/b = a * b^-1 is commutative?

[Eric Wieser]

It's false

[Eric Wieser]

It amounts to stating that multiplication is commutative, but you didn't require it to be.

[Eric Wieser]

docs#comm_group satisfies the property you need

[Shadman Sakib]

Well, I was using this proof to show that ((⇑angle_to_circle (⇑(zmod_to_angle hm) i))⁻¹ * ⇑angle_to_circle (⇑(zmod_to_angle hm) j)) = (⇑angle_to_circle (⇑(zmod_to_angle hm) j) / ⇑angle_to_circle (⇑(zmod_to_angle hm) i))

[Shadman Sakib]

I can supply an mwe in one moment

[Shadman Sakib]

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric

noncomputable theory

open complex dihedral_group

variables (n : ℝ) {m : ℕ}

def angle_to_circle_hom : real.angle ≃+ additive circle :=
(quotient_add_group.equiv_quotient_of_eq (by { ext x, exact exp_map_circle_eq_one_iff.symm})).trans
(quotient_add_group.quotient_ker_equiv_of_surjective exp_map_circle_hom exp_map_circle_surjective)

def angle_to_circle : real.angle ≃ circle := angle_to_circle_hom.to_equiv

def zmod_to_angle (hm : m ≠ 0) : zmod m →+ real.angle :=
zmod.lift m ⟨gmultiples_hom real.angle ↑(2 * real.pi /m),
  begin
    suffices : m • (2 * π / ↑m) = 2 * π,
    { simpa using congr_arg (coe : _ → real.angle) this },
    have : (m:ℝ) ≠ 0 := by exact_mod_cast hm,
    field_simp,
    ring
  end⟩

variables (hm : m ≠ 0)

lemma comm_angle_to_circle_zmod (i j : zmod m): ((angle_to_circle ((zmod_to_angle hm) i))⁻¹ * angle_to_circle ((zmod_to_angle hm) j)) =
(angle_to_circle ((zmod_to_angle hm) j) / angle_to_circle ((zmod_to_angle hm) i)) :=
begin
  sorry,
end

[Shadman Sakib]

Is there a way to show this with the structure comm_group?

[Eric Rodriguez]

what about (0 : real.angle)?

[Eric Rodriguez]

(also your mwe doesn't work, I can't find angle_to_circle_hom and you need the variables {m} higher up

[Shadman Sakib]

Ok, sorry about that. Please try it now