Zulip Chat Archive

Stream: maths

Topic: to_additive multiplicative


view this post on Zulip Patrick Massot (Oct 09 2018 at 13:42):

This is again a question about the machinery allowing to transfer stuff from multiplicative monoids/groups to additive. I'm trying to get a version of https://github.com/leanprover/mathlib/blob/master/group_theory/submonoid.lean#L112-L142 for groups. I tried:

import group_theory.subgroup

namespace group
variables {α : Type*} [group α]
theorem exists_list_of_mem_closure {s : set α} {a : α} (h : a  closure s) :
  (l:list α, (xl, x  s  x⁻¹  s)  l.prod = a) :=
begin
  induction h,
  case in_closure.basic : a ha { existsi ([a]), simp [ha] },
  case in_closure.one { existsi ([]), simp },
  case in_closure.mul : a b _ _ ha hb {
    rcases ha with la, ha, eqa,
    rcases hb with lb, hb, eqb,
    existsi (la ++ lb),
    simp [eqa.symm, eqb.symm, or_imp_distrib],
    exact assume a, ha a, hb a
  },
  case in_closure.inv : a a_in_clo hlist {
    rcases hlist with la, ha, eqa,
    existsi (la.reverse.map (λ x, x⁻¹)),
    split,
    { intros x x_in,
      rw list.mem_map at x_in,
      rcases x_in with b, b_in, hb,
      rw list.mem_reverse at b_in,
      specialize ha b b_in,
      have hb' : b = x⁻¹, by rw hb ; simp,
      rw [hb, hb'] at ha,
      cc },
    { rw [eqa, inv_prod la] } }
end
end group

namespace add_group
variables {α : Type*} [add_group α]

theorem exists_list_of_mem_closure {s : set α} {a : α} (h : a  closure s) :
  (l:list α, (xl, x  s  -x  s)  l.sum = a) :=
@group.exists_list_of_mem_closure (multiplicative α) _ _ _ _

end add_group

view this post on Zulip Patrick Massot (Oct 09 2018 at 13:43):

But Lean doesn't accept the second statement


Last updated: May 12 2021 at 08:14 UTC