Cast

📁 Source: Mathlib/Data/Nat/Choose/Cast.lean

Statistics

Metric	Count
Definitions	0
Theorems cast_add_choose, cast_choose, cast_choose_two	3
Total	3

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_add_choose 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring choose DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero factorial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	cast_choose
cast_choose 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring choose DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero factorial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	cast_ne_zero LT.lt.ne' factorial_pos eq_div_iff_mul_eq mul_ne_zero GroupWithZero.noZeroDivisors mul_assoc choose_mul_factorial_mul_factorial
cast_choose_two 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing choose DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toOne instOfNatAtLeastTwo instAtLeastTwoHAddOfNat	—	instAtLeastTwoHAddOfNat cast_descFactorial_two descFactorial_eq_factorial_mul_choose factorial_two mul_comm cast_mul cast_two eq_div_iff_mul_eq two_ne_zero

---

← Back to Index