Commit 2023-09-20 14:54 a959734f

View on Github →

feat: Nat.lcm_mul_left and Nat.lcm_mul_right (#6990) Add two lemmas about Nat.lcm. These results mirror Nat.gcd_mul_left present in Std.

Estimated changes

Modified Mathlib/Data/Int/GCD.lean

added theorem Int.lcm_mul_left

added theorem Int.lcm_mul_right

Modified Mathlib/Data/Nat/GCD/Basic.lean

added theorem Nat.lcm_mul_left

added theorem Nat.lcm_mul_right