Theorems · Definition · commutative algebra

EuclideanDomain.lcm

{R : Type u} → [EuclideanDomain R] → [DecidableEq R] → R → R → R

lcm a b is a (non-unique) element such that a ∣ lcm a b b ∣ lcm a b, and for any element c such that a ∣ c and b ∣ c, then lcm a b ∣ c

Defined in

Mathlib.Algebra.EuclideanDomain.Defs

Cited by

8 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

EuclideanDomainDecidableEq