Zulip Chat Archive

Stream: maths

Topic: zero ideal


view this post on Zulip Patrick Massot (Dec 17 2018 at 14:50):

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

view this post on Zulip Johan Commelin (Dec 17 2018 at 14:50):

I guess it is now

view this post on Zulip Patrick Massot (Dec 17 2018 at 14:51):

Thanks

view this post on Zulip Patrick Massot (Dec 17 2018 at 14:51):

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

view this post on Zulip Kenny Lau (Dec 17 2018 at 14:52):

lol

view this post on Zulip Kenny Lau (Dec 17 2018 at 14:52):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Dec 17 2018 at 14:56):

what binder types?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Dec 17 2018 at 14:58):

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

view this post on Zulip Kenny Lau (Dec 17 2018 at 14:58):

because we want to write I.mul_mem_left _ _

view this post on Zulip Patrick Massot (Dec 17 2018 at 15:00):

And how does it guess who is a?

view this post on Zulip Kenny Lau (Dec 17 2018 at 15:01):

from the type

view this post on Zulip Patrick Massot (Dec 17 2018 at 15:03):

hmm


Last updated: May 09 2021 at 10:11 UTC