mathlib3
5c8243f9 - fix(algebra/group/type_tags): resolve an instance diamond caused by over-eager unfolding (#11240)

Commit
4 years ago
fix(algebra/group/type_tags): resolve an instance diamond caused by over-eager unfolding (#11240) By setting the `one` and `zero` fields manually, we ensure that they are syntactically equal to the ones found via `has_one` and `has_zero`, rather than potentially having typeclass arguments resolved in a different way. This seems to fix the failing test. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Diamond.20in.20multiplicative.20nat/near/266824443)
Author
Parents
Loading