## Stream: maths

### Topic: multiplicative annoyance

#### 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.

#### 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

#### Kevin Buzzard (Mar 09 2019 at 23:32):

turned out it was mul_zero

#### Mario Carneiro (Mar 09 2019 at 23:36):

does add_group.closure have a defined recursor?

#### Mario Carneiro (Mar 09 2019 at 23:37):

in_closure.rec_on

#### 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