Theorem Ideal.fst_comp_quotientMulEquivQuotientProd

Modification history

2024-06-06 14:15
Mathlib/RingTheory/Ideal/QuotientOperations.lean
fix: remove Dedekind domain assumption from Ideal.inf_eq_mul_of_coprime (#13308)
Added Ideal.fst_comp_quotientMulEquivQuotientProdView on Github →