Zulip Chat Archive

Stream: maths

Topic: zero in subring


view this post on Zulip Patrick Massot (Sep 18 2018 at 15:13):

I just added to the perfectoid project:

instance subring_has_zero (R : Type*) [comm_ring R] (S : set R) [HS : is_subring S] : has_zero S :=
⟨⟨0, is_add_submonoid.zero_mem S⟩⟩

It seems this used to be unnecessary. Any idea what happened? Trying apply_instance loops forever


Last updated: May 18 2021 at 08:14 UTC