Theorem Associates.gcd_mk_mk

Modification history

2024-04-06 14:26
Mathlib/Algebra/GCDMonoid/Basic.lean
feat: GCDMonoid (Associates α) instance (#11618)
Added Associates.gcd_mk_mkView on Github →