GCD_and_LCM_Distribute_Over_Each_Other
Proveddistributive-operationsgreatest-common-divisorlowest-common-multipleproofwiki
lcm(a, gcd(b,c)) = gcd(lcm(a,b), lcm(a,c)) and gcd(a, lcm(b,c)) = lcm(gcd(a,b), gcd(a,c)).
Preamble
import Mathlib.Data.Nat.GCD.Basic
Formal statement
theorem GCD_and_LCM_Distribute_Over_Each_Other (a b c : ℕ) : Nat.lcm a (Nat.gcd b c) = Nat.gcd (Nat.lcm a b) (Nat.lcm a c) := by sorry
Source