SuperFactorial

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

Statistics

Metric	Count
Definitions superFactorial, termSf_	2
Theorems prod_Icc_factorial, prod_range_factorial_succ, prod_range_succ_factorial, superFactorial_four_mul, superFactorial_one, superFactorial_succ, superFactorial_two, superFactorial_two_mul, superFactorial_zero	9
Total	11

Nat

Definitions

Name	Category	Theorems
superFactorial 📖	CompOp	11 math math: prod_range_factorial_succ, superFactorial_zero, prod_Icc_factorial, Matrix.superFactorial_dvd_vandermonde_det, superFactorial_two_mul, Matrix.det_vandermonde_id_eq_superFactorial, superFactorial_succ, superFactorial_four_mul, superFactorial_one, superFactorial_two, prod_range_succ_factorial
termSf_ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_Icc_factorial 📖	mathematical	—	Finset.prod instCommMonoid Finset.Icc instPreorder instLocallyFiniteOrder factorial superFactorial	—	Finset.Ico_add_one_right_eq_Icc instNoMaxOrder Finset.prod_Ico_succ_top le_add_self instCanonicallyOrderedAdd factorial_succ superFactorial.eq_2 factorial.eq_2 mul_comm
prod_range_factorial_succ 📖	mathematical	—	Finset.prod instCommMonoid Finset.range factorial superFactorial	—	Finset.prod_Ico_add' instIsOrderedCancelAddMonoid CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd Finset.range_eq_Ico prod_Icc_factorial
prod_range_succ_factorial 📖	mathematical	—	Finset.prod instCommMonoid Finset.range factorial superFactorial	—	Finset.prod_range_succ mul_comm superFactorial.eq_2
superFactorial_four_mul 📖	mathematical	—	superFactorial Monoid.toNatPow instMonoid Finset.prod instCommMonoid Finset.range factorial	—	superFactorial_two_mul mul_assoc pow_mul' mul_pow
superFactorial_one 📖	mathematical	—	superFactorial	—	—
superFactorial_succ 📖	mathematical	—	superFactorial factorial	—	—
superFactorial_two 📖	mathematical	—	superFactorial	—	—
superFactorial_two_mul 📖	mathematical	—	superFactorial Monoid.toNatPow instMonoid Finset.prod instCommMonoid Finset.range factorial	—	mul_add Distrib.leftDistribClass mul_one Finset.prod_congr Finset.prod_range_succ mul_pow Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one
superFactorial_zero 📖	mathematical	—	superFactorial	—	—

---

← Back to Index