Theorem Algebra.TensorProduct.quotIdealMapEquivQuotTensor_mk

Modification history

2026-03-26 08:33
Mathlib/RingTheory/TensorProduct/Quotient.lean
feat(RingTheory/Unramified/Dedekind): a domain finite and unramified over a Dedekind domain is a Dedekind domain (#36838) …
Added Algebra.TensorProduct.quotIdealMapEquivQuotTensor_mkView on Github →