Theorems · Theorem · number theory
IsUnit.natCast_of_isNilpotent_of_coprime
∀ {A : Type u_1} [inst : CommRing A] {n p : ℕ}, IsNilpotent ↑p → p.Coprime n → IsUnit ↑n- Defined in
- Mathlib.Data.Nat.Factorial.NatCast
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 39 from the axioms · uses propext, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Nat.cast_oneproof · cited by 2,501
- zero_addproof · cited by 2,366
- MulZeroClass.zero_mulproof · cited by 1,625
- IsUnitstatement · cited by 1,602
- Int.cast_natCastproof · cited by 393
- Int.cast_oneproof · cited by 371
- IsNilpotentstatement and proof · cited by 248
- Nat.cast_powproof · cited by 131
- Int.cast_powproof · cited by 59
- IsUnit.of_mul_eq_oneproof · cited by 43
- Nat.gcdAproof · cited by 23
Cited by1
Results whose statement or proof uses this declaration.
- IsUnit.natCast_factorial_of_isNilpotentproof · cited by 0