Theorems · Theorem · number theory
Nat.factorization_lcm
∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (a.lcm b).factorization = a.factorization ⊔ b.factorization- Defined in
- Mathlib.Data.Nat.Factorization.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsuppstatement and proof · cited by 5,255
- Finsupp.extproof · cited by 399
- Nat.factorizationstatement and proof · cited by 215
- add_right_injproof · cited by 71
- Nat.factorization_mulproof · cited by 14
- Nat.factorization_gcdproof · cited by 2
- min_add_maxproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_applyproof · cited by 2
- Finset.factorization_lcmproof · cited by 1
- Nat.factorizationLCMRight_dvd_rightproof · cited by 1
- Nat.factorizationLCMLeft_dvd_leftproof · cited by 1