Zulip Chat Archive
Stream: new members
Topic: Lattice of Ideals has Bottom
Ken Lee (Dec 05 2019 at 17:29):
Where can I find lattice.has_bot (ideal A) where A is a commutative ring?
Kevin Buzzard (Dec 05 2019 at 17:31):
Maybe instance : lattice.has_bot (ideal A) := by dunfold ideal; apply_instance?
Patrick Massot (Dec 05 2019 at 17:32):
#check (by apply_instance : lattice.has_bot (ideal A))
Ken Lee (Dec 05 2019 at 17:32):
thanks!
Last updated: Dec 20 2023 at 11:08 UTC