Commit 2025-02-16 15:58 6df878a6

View on Github →

chore(*): fix some Fintype/DecidableEq linter errors (#21943)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

Modified Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean

modified theorem AddChar.expect_apply_eq_ite

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added theorem SimpleGraph.Subgraph.neighborSet_eq_of_equiv

Modified Mathlib/Data/Matroid/Rank/Finite.lean

modified theorem Matroid.IsRkFinite.iUnion

Modified Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean

Modified Mathlib/Probability/Integration.lean

modified theorem ProbabilityTheory.lintegral_prod_eq_prod_lintegral_of_indepFun