## Stream: maths

### Topic: zero ideal

#### Patrick Massot (Dec 17 2018 at 14:50):

I lost the zero ideal during the module refactor. Does anyone know where it ended up?

#### Johan Commelin (Dec 17 2018 at 14:50):

I guess it is now ⊥

Thanks

#### Patrick Massot (Dec 17 2018 at 14:51):

I'm a very slow learner. I was looking for something named zero

lol

#### Kenny Lau (Dec 17 2018 at 14:52):

"I lost something" -- what is it? "I lost the zero ideal"

#### Johan Commelin (Dec 17 2018 at 14:52):

I'm a very slow learner. I was looking for something named zero

That would be too easy.

#### Patrick Massot (Dec 17 2018 at 14:52):

Who would think that zero is a more natural thing than the bottom of a lattice nowadays?

#### Patrick Massot (Dec 17 2018 at 14:55):

ideal.mul_mem_left : ∀ {α : Type u_1} [_inst_1 : comm_ring α] (I : ideal α) {a b : α}, b ∈ I → a * b ∈ I What happened to binder types here?

#### Kenny Lau (Dec 17 2018 at 14:56):

what binder types?

#### Patrick Massot (Dec 17 2018 at 14:58):

Why not

lemma ideal.mul_mem_left' {α : Type*} [comm_ring α] {I : ideal α} (a : α) {b : α} (h : b ∈ I) : a * b ∈ I :=
ideal.mul_mem_left _ h


#### Patrick Massot (Dec 17 2018 at 14:58):

Like, I want a and b ∈ I to be explicit, and everything else implicit

#### Kenny Lau (Dec 17 2018 at 14:58):

because we want to write I.mul_mem_left _ _

#### Patrick Massot (Dec 17 2018 at 15:00):

And how does it guess who is a?

from the type

#### Patrick Massot (Dec 17 2018 at 15:03):

hmm

Last updated: May 09 2021 at 10:11 UTC