Theorems · Theorem · number theory
isUnit_of_dvd_one
∀ {α : Type u_1} [inst : CommMonoid α] {a : α}, a ∣ 1 → IsUnit a- Defined in
- Mathlib.Algebra.Divisibility.Units
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
- Assumes
- CommMonoid
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.
- CommMonoidstatement and proof · cited by 2,264
- IsUnitstatement · cited by 1,602
- isUnit_iff_dvd_oneproof · cited by 21
Cited by18
Results whose statement or proof uses this declaration.
- Prime.irreducibleproof · cited by 54
- Prime.dvd_of_dvd_powproof · cited by 14
- Prime.not_dvd_oneproof · cited by 6
- Matrix.isUnit_charpolyRev_of_isNilpotentproof · cited by 2
- ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAuxproof · cited by 2
- IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdealproof · cited by 2
- dvd_and_not_dvd_iffproof · cited by 2
- exists_eq_pow_of_mul_eq_pow_of_coprimeproof · cited by 1
- pow_dvd_of_mul_eq_powproof · cited by 1
- isInteger_of_is_root_of_monicproof · cited by 1
- UniqueFactorizationMonoid.exists_dvd_pow_iff_radical_dvdproof · cited by 1
- Polynomial.Monic.isUnit_leadingCoeff_of_dvdproof · cited by 1