Theorems · Theorem · commutative algebra
Squarefree.squarefree_of_dvd
∀ {R : Type u_1} [inst : Monoid R] {x y : R}, x ∣ y → Squarefree y → Squarefree x- Defined in
- Mathlib.Algebra.Squarefree.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- Dvd.dvd.transproof · cited by 148
- Squarefreestatement and proof · cited by 112
Cited by15
Results whose statement or proof uses this declaration.
- BoundingSieve.nu_inv_eq_sum_divisors_inv_selbergTermsproof · cited by 2
- Squarefree.dvd_of_squarefree_of_mul_dvd_mul_rightproof · cited by 2
- BoundingSieve.prod_primeFactors_nuproof · cited by 2
- Nat.squarefree_pow_iffproof · cited by 2
- Squarefree.pow_dvd_of_pow_dvdproof · cited by 1
- Associated.squarefree_iffproof · cited by 1
- Squarefree.eq_zero_or_one_of_pow_of_not_isUnitproof · cited by 1
- Nat.divisors_filter_squarefree_of_squarefreeproof · cited by 1
- BoundingSieve.squarefree_of_dvd_prodPrimesproof · cited by 1
- BoundingSieve.nu_lt_one_of_dvd_prodPrimesproof · cited by 0
- Nat.grahamConjecture_of_squarefreeproof · cited by 0
- Squarefree.gcd_leftproof · cited by 0