Zulip Chat Archive

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

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

Thanks

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

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

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

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?

Kenny Lau (Dec 17 2018 at 15:01):

from the type

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

hmm


Last updated: Dec 20 2023 at 11:08 UTC