leanprover-community / mathlib

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

Zulip Chat Archive

Stream: maths

Topic: base change for modules


Reid Barton (Feb 14 2019 at 05:33):

We don't yet have S⊗RMS \otimes_R MS⊗R​M as an SSS-module for SSS an RRR-algebra, right?

Kenny Lau (Feb 14 2019 at 05:39):

An obscure version of that statement (with M and SxM being algberas) is in an obscure repo of mine


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll