ℕ is a normalized GCD monoid.

instance instGCDMonoidNat : 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 = m.gcd n

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

instance instNormalizedGCDMonoidNat : NormalizedGCDMonoid ℕ

Equations

• instNormalizedGCDMonoidNat = let __src := inferInstance; let __src_1 := inferInstance; NormalizedGCDMonoid.mk instNormalizedGCDMonoidNat.proof_1 instNormalizedGCDMonoidNat.proof_2