Revision #3005 → #3238 · back to history
modifiedLCM from GCD formula45e6e96a22e9
| Field | From #3005 | To #3238 |
|---|
| mathlib.decl | gcd_mul_lcm | GCDMonoid.gcd_mul_lcm |
| provenance | ai | ai-moderated |
modifiedEquivalent LCM-GCD formulasae388f46fac5
| Field | From #3005 | To #3238 |
|---|
| mathlib.decl | gcd_mul_lcm | GCDMonoid.gcd_mul_lcm |
| provenance | ai | ai-moderated |
modifiedLCM-GCD formula with zero arguments6ca8412ae60a
| Field | From #3005 | To #3238 |
|---|
| mathlib.decl | gcd_mul_lcm | GCDMonoid.gcd_mul_lcm |
| provenance | ai | ai-moderated |
modifiedLCM identity for nonzero arguments402791c39852
| Field | From #3005 | To #3238 |
|---|
| mathlib.decl | gcd_mul_lcm | GCDMonoid.gcd_mul_lcm |
| provenance | ai | ai-moderated |