Zulip Chat Archive

Stream: new members

Topic: coe one


Maxime Darrin (Jul 16 2021 at 20:46):

HI,
I want to apply nat.mul_one to an hypothesis involving pnats using rw, how can I somehow cast a pnat into a nat

import data.pnat.basic

theorem USAJMO_Problems_Problem_1 :
  forall f: pnat -> pnat,
  (forall (a b: pnat), f(a*a + b*b) = f(a)* f(b) /\ f(a*a) = f(a)*f(a))
  -> forall n, f n = 1 :=
  begin
  intro f,
  intro ab,

  have f1 : f(1) = 1,
  have f2 : f (1*1) = (f 1)*(f 1),
  exact and.elim_right (ab 1 1),
  rw nat.mul_one at f2,

Eric Rodriguez (Jul 16 2021 at 20:48):

you can just use the more general mul_one, which works for all groups

Eric Rodriguez (Jul 16 2021 at 20:49):

(weaker, even!)

Maxime Darrin (Jul 16 2021 at 20:53):

Oh thx !


Last updated: Dec 20 2023 at 11:08 UTC