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: May 02 2025 at 03:31 UTC