## Stream: maths

### Topic: zero in subring

#### 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 :=

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