Theorem Nat.prod_range_factorial_succ

Modification history

2024-05-27 08:32
Mathlib/Data/Nat/Factorial/SuperFactorial.lean
chore: Use the new `∑ i ∈ s, f i` notation (#13209) …
Modified Nat.prod_range_factorial_succView on Github →
2024-02-09 22:56
Mathlib/Data/Nat/Factorial/SuperFactorial.lean
chore: tidy various files (#10362)
Modified Nat.prod_range_factorial_succView on Github →
2024-01-25 13:08
Mathlib/Data/Nat/Factorial/SuperFactorial.lean
feat: superFactorial_two_mul, superFactorial_four_mul (#7924)
Modified Nat.prod_range_factorial_succView on Github →
2023-09-26 17:18
Mathlib/Data/Nat/Factorial/SuperFactorial.lean
feat: super factorial written as product (#6806)
Added Nat.prod_range_factorial_succView on Github →