Zulip Chat Archive

Stream: mathlib4

Topic: simpNF and MulOpposite


Antoine Labelle (Dec 14 2022 at 16:57):

In #1001, the simpNF linter gives me the following error:

#check smul_eq_mul_unop /- Left-hand side simplifies from
  a • a'
to
  a * a'
using
  simp only [smul_eq_mul]
Try to change the left-hand side to the simplified term!
 -/

Here is the relevant lemma:

@[simp, to_additive]
theorem MulOpposite.smul_eq_mul_unop [Mul α] {a : αᵐᵒᵖ} {a' : α} : a  a' = a' * a.unop :=
  rfl

That seems very weird to me because a has type αᵐᵒᵖ while a' has type α, so the multiplication a * a' shouldn't be defined (and indeed if I try replacing a • a' by a * a' I get an error failed to synthesize instance HMul αᵐᵒᵖ α ?m.5162 as I would expect). What is going on here?

Jireh Loreaux (Dec 14 2022 at 17:11):

Well, αᵐᵒᵖ is a type synonym for α, so I imagine that in a * a' that a : α. You should be able to see it with whatever the mathlib4 equivalent of set_option pp.all true is.

Antoine Labelle (Dec 14 2022 at 17:24):

Well a : αᵐᵒᵖ definitely shouldn't be interpreted as an element of α when interpreting a • a', because, despite being type synonyms αᵐᵒᵖ and α both have a scalar action on α and these are two different actions (left and right multiplication).


Last updated: Dec 20 2023 at 11:08 UTC