leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: What do I import to get linear_map.add_comm_monoid


Eric Wieser (Oct 30 2020 at 12:26):

The docs are out of date, and the source link for docs#linear_map.add_comm_monoid is broken

Eric Wieser (Oct 30 2020 at 12:29):

(the link is broken I think because (a) the git SHA is ambigious, and (b) @Anne Baanen moved it and the docs are stale)

Eric Wieser (Oct 30 2020 at 12:34):

Ah, looks like they just rebuilt


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll