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