Zulip Chat Archive

Stream: maths

Topic: has_mul instance for option?


view this post on Zulip Koundinya Vajjha (Jul 10 2019 at 20:55):

Does option have a has_mul instance?

I've been trying to prove the following:

lemma to_nnreal_mul (a b : ennreal) : ennreal.to_nnreal (a * b) = (ennreal.to_nnreal a)*(ennreal.to_nnreal b) := sorry

But after cases on both a and b I want to simplify the none * some term and the others, but I am stuck. Any suggetions?

view this post on Zulip Chris Hughes (Jul 10 2019 at 21:09):

none is defeq to \top, and there should be lemmas about that. Probably rfl will prove it. There might be a special version of cases for ennreal

view this post on Zulip Koundinya Vajjha (Jul 10 2019 at 21:21):

I'm stuck on ennreal.to_nnreal (some a * some b) = a * b.

view this post on Zulip Sebastien Gouezel (Jul 10 2019 at 21:43):

lemma to_nnreal_mul (a b : ennreal) :
  ennreal.to_nnreal (a * b) = (ennreal.to_nnreal a) * (ennreal.to_nnreal b) :=
begin
  cases a; cases b,
  { simp [none_eq_top] },
  { by_cases h : b = 0; simp [none_eq_top, some_eq_coe, h, top_mul] },
  { by_cases h : a = 0; simp [none_eq_top, some_eq_coe, h, mul_top] },
  { simp [some_eq_coe, coe_mul.symm, -coe_mul] }
end

We should probably add a simp attribute to none_eq_top and some_eq_coe, by the way.


Last updated: May 14 2021 at 20:13 UTC