ℕ is a normalized GCD monoid.

instance instGCDMonoidNatInstCancelCommMonoidWithZero : GCDMonoid ℕ

ℕ is a gcd_monoid.

Equations

• One or more equations did not get rendered due to their size.

theorem gcd_eq_nat_gcd (m : ℕ) (n : ℕ) : gcd m n = Nat.gcd m n

theorem lcm_eq_nat_lcm (m : ℕ) (n : ℕ) : lcm m n = Nat.lcm m n

instance instNormalizedGCDMonoidNatInstCancelCommMonoidWithZero : NormalizedGCDMonoid ℕ

Equations

• One or more equations did not get rendered due to their size.