## Stream: new members

### Topic: diamond

#### Yakov Pechersky (Aug 31 2021 at 13:37):

On my branch#pechersky/ordered-module-smul, I am hitting a diamond on smul actions on order_dual. But it seems that the data (the actual smul) is the same. What's going on here? Is this another instance of how use of defeq of R and order_dual R causes issues later on?

import algebra.module.ordered

section semiring

variables (k E : Type*)
[hr : semiring k] [hc : ordered_add_comm_group E] [hm : module k E]

def LHS :=
(@order_dual.smul_with_zero k E hr
(@mul_action_with_zero.to_smul_with_zero k E
(@semiring.to_monoid_with_zero k hr)
(@module.to_mul_action_with_zero k E hr
hm)))

def RHS :=
(@mul_action_with_zero.to_smul_with_zero k (order_dual E)
(@semiring.to_monoid_with_zero k hr)
(@module.to_mul_action_with_zero k (order_dual E) hr
(@order_dual.module k E hr
hm)))

#check @LHS k E hr hc hm
/-
LHS k E : smul_with_zero k (order_dual E)
-/

#check @RHS k E hr hc hm
/-
RHS k E : smul_with_zero k (order_dual E)
-/

attribute [ext] smul_with_zero has_scalar

lemma fails : @LHS k E hr hc hm = @RHS k E hr hc hm := rfl

lemma succeed : @LHS k E hr hc hm = @RHS k E hr hc hm :=
begin
ext1,
ext1,
refl
end

end semiring


#### Yakov Pechersky (Aug 31 2021 at 14:19):

Yes, seems so. Being less defeq-y, one avoids it. #8930, #8938

Last updated: Dec 20 2023 at 11:08 UTC