Zulip Chat Archive

Stream: maths

Topic: multiplicative annoyance


view this post on Zulip Kevin Buzzard (Mar 09 2019 at 23:31):

import group_theory.subgroup

example (R : Type*) [comm_ring R] (P : R  Prop) (T : set R)
  (HP1 :  t : R, t  T  P t) (HP2 : P 0) (HP3 :  r : R, P r  P (-r))
  (HP4 :  r s : R, P r  P s  P (r + s))
 (u : R) (hu : u  add_group.closure T) : P u :=
begin
  induction hu with a ha a ha ih a b ha hb iha ihb,
  { exact HP1 a ha},
  { -- goal P 1
    exact HP2},
  { -- goal P a⁻¹
    exact HP3 a ih,
  },
  { -- goal P (a * b)
    exact HP4 a b iha ihb,
  }
end

All the goals are multiplicative.

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 23:32):

In real life I have much more complex goals, and I just failed to use mul_one to deal with v * 1 and then I realised that it might be any of mul_zero, add_one or add_zero

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 23:32):

turned out it was mul_zero

view this post on Zulip Mario Carneiro (Mar 09 2019 at 23:36):

does add_group.closure have a defined recursor?

view this post on Zulip Mario Carneiro (Mar 09 2019 at 23:37):

in_closure.rec_on

view this post on Zulip Kenny Lau (Mar 09 2019 at 23:41):

this is all XXX's fault of not allowing variable operation


Last updated: May 18 2021 at 08:14 UTC