Theorem Ideal.pi_tensorProductMk_quotient_surjective

Modification history

2025-11-04 08:07
Mathlib/RingTheory/Ideal/Quotient/ChineseRemainder.lean
feat(RingTheory): finite flat constant rank module over semilocal ring is free (#31241) …
Added Ideal.pi_tensorProductMk_quotient_surjectiveView on Github →