mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(RingTheory/Flat): faithfully flat ring maps

Open judithludwig opened this issue 1 year ago • 10 comments

Add definition of faithfully flat ring maps and show basic properties. Co-authored-by: Florent Schaffhauser (github: matematiflo) Co-authored-by: Jujian Zhang (github:@jjaassoonn) Co-authored-by: Yunzhou Xie (github:@whysoserioushah)

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

  • [x] depends on: #17803
  • [x] depends on: #17805
  • [x] depends on: #17484
  • [x] depends on: #17869

Open in Gitpod

judithludwig avatar Jul 22 '24 13:07 judithludwig