Commit 2025-03-21 15:47 bdf8f646

View on Github →

chore: adjust hypothesis of mul_factorial_pred (#23160) We generally prefer nonzeroness as a hypothesis.

Estimated changes

Modified Archive/Imo/Imo1987Q1.lean

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

modified theorem Nat.mul_factorial_pred

Modified Mathlib/GroupTheory/IndexNormal.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean

Modified Mathlib/RingTheory/DividedPowers/Basic.lean