## Stream: maths

### Topic: local rings

#### Johan Commelin (Mar 05 2019 at 18:08):

@Mario Carneiro Is there a reason why you are not using the type class system for is_local_ring here?

def nonunits_ideal (h : is_local_ring α) : ideal α :=
{ carrier := nonunits α,
zero := zero_mem_nonunits.2 h.zero_ne_one,
rcases id h with ⟨M, mM, hM⟩,
have : ∀ x ∈ nonunits α, x ∈ M,
{ intros x hx,
rcases (ideal.span {x} : ideal α).exists_le_maximal _ with ⟨N, mN, hN⟩,
{ cases hM N mN,
rwa [ideal.span_le, singleton_subset_iff] at hN },
{ exact mt ideal.span_singleton_eq_top.1 hx } },
intros x y hx hy,
exact coe_subset_nonunits mM.1 (M.add_mem (this _ hx) (this _ hy))
end,
smul := λ a x, mul_mem_nonunits_right }


#### Mario Carneiro (Mar 05 2019 at 19:22):

is is_local_ring a class? I don't think it was when I wrote that

#### Mario Carneiro (Mar 05 2019 at 19:23):

actually it might be one of those "not really a class" classes like nat.prime

#### Mario Carneiro (Mar 05 2019 at 19:24):

it's only used instance implicit when it needs to be for some other instance

#### Johan Commelin (Mar 07 2019 at 08:51):

@Mario Carneiro Hmmm, I see. What is the objection to treating this a an "actually really a class" class?

Last updated: May 18 2021 at 07:19 UTC