Commit 2024-04-06 14:26 92f24cbd

View on Github →

feat: GCDMonoid (Associates α) instance (#11618)

Estimated changes

added theorem Associates.mk_quot_out
added theorem Associated.gcd
added theorem Associated.lcm
added theorem Associates.gcd_mk_mk
added theorem Associates.lcm_mk_mk