NatCast

📁 Source: Mathlib/Data/Nat/Factorial/NatCast.lean

Statistics

Metric	Count
Definitions	0
Theorems natCast_factorial_iff_of_charP, natCast_factorial_of_algebra, natCast_factorial_of_isNilpotent, natCast_factorial_of_le, natCast_factorial_of_lt, natCast_of_isNilpotent_of_coprime, castChoose_eq	7
Total	7

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCast_factorial_iff_of_charP 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial	—	Fact.out Nat.cast_one Nat.Prime.pos Nat.factorial_succ Nat.cast_mul Commute.isUnit_mul_iff Nat.cast_commute CharP.isUnit_natCast_iff lt_of_le_of_ne dvd_rfl LT.lt.le
natCast_factorial_of_algebra 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.factorial	—	Nat.factorial_ne_zero map_natCast RingHom.instRingHomClass map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
natCast_factorial_of_isNilpotent 📖	mathematical	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	IsUnit Nat.factorial	—	Nat.cast_one Nat.cast_mul instIsDedekindFiniteMonoid natCast_of_isNilpotent_of_coprime Nat.Prime.coprime_iff_not_dvd Fact.out
natCast_factorial_of_le 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.factorial	—	—	ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd add_zero add_right_comm add_assoc Commute.isUnit_mul_iff Nat.cast_commute Nat.cast_mul Nat.factorial_succ
natCast_factorial_of_lt 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.factorial	—	—	natCast_factorial_of_le
natCast_of_isNilpotent_of_coprime 📖	mathematical	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	IsUnit	—	Nat.cast_one Nat.cast_pow Int.cast_pow Int.cast_natCast Int.cast_one Nat.gcd_eq_gcd_ab of_mul_eq_one instIsDedekindFiniteMonoid MulZeroClass.zero_mul zero_add

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
castChoose_eq 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring factorial Finset Finset.instMembership Finset.HasAntidiagonal.antidiagonal instAddMonoid Finset.Nat.instHasAntidiagonal	choose Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Ring.inverse	—	Ring.eq_mul_inverse_iff_mul_eq IsUnit.natCast_factorial_of_le cast_mul add_comm add_choose_mul_factorial_mul_factorial Finset.HasAntidiagonal.mem_antidiagonal

---

← Back to Index