mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard
verified publisher icon leanprover-community

feat(RingTheory/DedekindDomain/Ideal): add two lemmas about the multiplicity of normalized factors

Open faenuccio opened this issue 1 year ago • 0 comments

Add two lemmas on the multiplicity of normalized factors in relation to principal ideals and the cardinality of associates.

Co-authored-by: María Inés de Frutos-Fernández @mariainesdff

Open in Gitpod

faenuccio avatar May 20 '24 17:05 faenuccio