Commit 2025-10-12 00:30 54c708e5

View on Github →

chore: adaptations for batteries#1456 (#30444)

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

deleted theorem Fin.coe_divNat

deleted theorem Fin.coe_modNat

deleted def Fin.divNat

deleted def Fin.modNat

Modified Mathlib/Logic/Equiv/Fin/Basic.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Binomial.lean

Modified lake-manifest.json