Commit 2025-04-28 14:19 111f5c15

View on Github →

chore(*): fix some Fintype/Finite assumptions (#24424) Found by the linter in #10235 Also drop a DecidableEq assumption and fix _inj vs _injective name.

Estimated changes

Modified Mathlib/Combinatorics/Nullstellensatz.lean

Modified Mathlib/Combinatorics/SimpleGraph/Diam.lean

modified theorem SimpleGraph.connected_iff_diam_ne_zero

Modified Mathlib/Data/DFinsupp/Defs.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/RepresentationTheory/Tannaka.lean

deleted theorem TannakaDuality.FiniteGroup.equivHom_inj

added theorem TannakaDuality.FiniteGroup.equivHom_injective

Modified Mathlib/RingTheory/LocalRing/NonLocalRing.lean

modified theorem IsLocalRing.not_isLocalRing_of_nontrivial_pi

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

modified theorem MvPolynomial.weightedTotalDegree_rename_of_injective