Commit 2023-09-19 14:59 fe39449a

View on Github →

chore: rm @simp from factorial (#7078)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Intervals.lean

Modified Mathlib/Analysis/Calculus/Taylor.lean

Modified Mathlib/Analysis/SpecialFunctions/Exponential.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

modified theorem Real.Gamma_two

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/Nat/Factorial/Basic.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

Modified Mathlib/NumberTheory/Bernoulli.lean

Modified Mathlib/NumberTheory/ZetaValues.lean