LCM

📁 Source: Mathlib/Data/Nat/Factorization/LCM.lean

Statistics

Metric	Count
Definitions	0
Theorems coprime_factorizationLCMLeft_factorizationLCMRight, factorizationLCMLeft_dvd_left, factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_pos, factorizationLCMLeft_zero_left, factorizationLCMLeft_zero_right, factorizationLCMRight_dvd_right, factorizationLCMRight_pos, factorizationLCMRight_zero_right, factorizationLCRight_zero_left	10
Total	10

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprime_factorizationLCMLeft_factorizationLCMRight 📖	mathematical	—	factorizationLCMLeft factorizationLCMRight	—	factorizationLCMLeft.eq_1 factorizationLCMRight.eq_1 coprime_prod_left_iff coprime_prod_right_iff coprime_pow_primes prime_of_mem_primeFactors Mathlib.Tactic.Contrapose.contrapose₄
factorizationLCMLeft_dvd_left 📖	mathematical	—	factorizationLCMLeft	—	eq_or_ne factorization_zero instCanonicallyOrderedAdd Unique.instSubsingleton factorization_prod_pow_eq_self Finsupp.prod_of_support_subset Finsupp.mem_support_iff factorization_lcm LT.lt.ne' lt_sup_iff pow_zero Finset.prod_dvd_prod_of_dvd pow_dvd_pow sup_le le_rfl one_dvd
factorizationLCMLeft_mul_factorizationLCMRight 📖	mathematical	—	factorizationLCMLeft factorizationLCMRight	—	factorization_prod_pow_eq_self factorizationLCMLeft.eq_1 factorizationLCMRight.eq_1 Finsupp.prod_mul mul_one one_mul
factorizationLCMLeft_pos 📖	mathematical	—	factorizationLCMLeft	—	factorizationLCMLeft.eq_1 Finsupp.prod_ne_zero_iff instNontrivial IsStrictOrderedRing.noZeroDivisors instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd isReduced_of_noZeroDivisors factorization_zero_right
factorizationLCMLeft_zero_left 📖	mathematical	—	factorizationLCMLeft	—	factorization_zero instCanonicallyOrderedAdd
factorizationLCMLeft_zero_right 📖	mathematical	—	factorizationLCMLeft	—	factorization_zero instCanonicallyOrderedAdd
factorizationLCMRight_dvd_right 📖	mathematical	—	factorizationLCMRight	—	eq_or_ne factorization_zero instCanonicallyOrderedAdd Unique.instSubsingleton factorization_prod_pow_eq_self Finsupp.prod_of_support_subset Finsupp.mem_support_iff factorization_lcm LT.lt.ne' lt_sup_iff pow_zero Finset.prod_dvd_prod_of_dvd one_dvd pow_dvd_pow sup_le LT.lt.le not_le le_rfl
factorizationLCMRight_pos 📖	mathematical	—	factorizationLCMRight	—	factorizationLCMRight.eq_1 Finsupp.prod_ne_zero_iff instNontrivial IsStrictOrderedRing.noZeroDivisors instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd isReduced_of_noZeroDivisors factorization_zero_right
factorizationLCMRight_zero_right 📖	mathematical	—	factorizationLCMRight	—	factorization_zero instCanonicallyOrderedAdd Finsupp.prod_fun_one
factorizationLCRight_zero_left 📖	mathematical	—	factorizationLCMRight	—	factorization_zero instCanonicallyOrderedAdd

---

← Back to Index