Theorems · Theorem · commutative algebra
Nat.finiteMultiplicity_iff
∀ {a b : ℕ}, FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b- Defined in
- Mathlib.RingTheory.Multiplicity
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- one_powproof · cited by 521
- lt_of_not_geproof · cited by 374
- not_ltproof · cited by 306
- not_iff_notproof · cited by 159
- not_and_orproof · cited by 82
- FiniteMultiplicitystatement · cited by 73
- not_lt_of_geproof · cited by 52
- zero_dvd_iffproof · cited by 37
- not_ne_iffproof · cited by 30
- Classical.by_contradictionproof · cited by 6
- FiniteMultiplicity.not_iff_forallproof · cited by 4
Cited by13
Results whose statement or proof uses this declaration.
- Nat.exists_eq_pow_mul_and_not_dvdproof · cited by 3
- Int.finiteMultiplicity_iffproof · cited by 2
- Int.emultiplicity_pow_sub_powproof · cited by 2
- Nat.Prime.emultiplicity_choose'proof · cited by 2
- Nat.Prime.emultiplicity_choose_prime_powproof · cited by 2
- Nat.emultiplicity_eq_card_pow_dvdproof · cited by 1
- le_padicValNat_iff_replicate_subperm_primeFactorsListproof · cited by 1
- Nat.Prime.emultiplicity_factorial_mul_succproof · cited by 1
- Nat.Prime.emultiplicity_selfproof · cited by 1
- Choose.eq_pow_multiplicity_of_choose_modEq_zeroproof · cited by 1
- Int.two_pow_sub_powproof · cited by 1
- Int.two_pow_sub_pow'proof · cited by 1