Theorem Module.Flat.tensorProduct_mk_injective

Modification history

2026-04-29 11:39
Mathlib/RingTheory/Flat/Basic.lean
feat: drop IsAlgClosed hypothesis from isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed (#38542) …
Added Module.Flat.tensorProduct_mk_injectiveView on Github →