Theorem Nat.coprime_prod_left

Modification history

2023-12-14 12:44
Mathlib/Data/Nat/GCD/BigOperators.lean
feat(Data/Nat/GCD/BigOperators): add lemmas about coprimality with `List.prod`, `Multiset.prod`, `Finset.prod` (#9005) …
Deleted Nat.coprime_prod_leftView on Github →
2023-08-10 19:52
Mathlib/Data/Nat/GCD/BigOperators.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified Nat.coprime_prod_leftView on Github →
2023-01-18 16:54
Mathlib/Data/Nat/GCD/BigOperators.lean
feat port: Data.Nat.GCD.BigOperators (#1649)
Added Nat.coprime_prod_leftView on Github →