mathlib
ee18af19 - feat(ring_theory/dedekind_domain): `gcd_monoid (ideal A)` in Dedekind domains (#17100)

Commit

3 years ago

feat(ring_theory/dedekind_domain): `gcd_monoid (ideal A)` in Dedekind domains (#17100) In fact, we show that all lawful GCD/LCM operations on ideals coincide with the supremum/infimum.

Author

Vierkantor

Parents

bdfa72be

mathlib ee18af19 - feat(ring_theory/dedekind_domain): `gcd_monoid (ideal A)` in Dedekind domains (#17100)

mathlib
ee18af19 - feat(ring_theory/dedekind_domain): `gcd_monoid (ideal A)` in Dedekind domains (#17100)