Theorem IsReduced.tensorProduct_of_flat_of_forall_fg

Modification history

2025-11-13 13:13
Mathlib/RingTheory/Flat/Basic.lean
feat: define geometrically reduced algebras (#27400) …
Added IsReduced.tensorProduct_of_flat_of_forall_fgView on Github →