Commit 2023-01-18 16:54 ebe63c71

View on Github →

feat port: Data.Nat.GCD.BigOperators (#1649)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/GCD/BigOperators.lean

added theorem Nat.coprime_prod_left

added theorem Nat.coprime_prod_right