Commit 2025-09-19 07:04 85c63035

View on Github →

chore(*): drop some Decidable/Fintype assumptions (#29785) Found by the linter in #10235

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/ProdHom.lean

modified theorem MonoidWithZeroHom.fst_surjective

modified theorem MonoidWithZeroHom.snd_surjective

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

modified theorem MvPolynomial.coe_coeffs_map

Modified Mathlib/Algebra/SkewMonoidAlgebra/Single.lean

modified theorem SkewMonoidAlgebra.coeff_update_ne

modified theorem SkewMonoidAlgebra.coeff_update_same

modified theorem SkewMonoidAlgebra.update_eq_erase_add_single

modified theorem SkewMonoidAlgebra.update_zero_eq_erase

Modified Mathlib/Algebra/SkewMonoidAlgebra/Support.lean

Modified Mathlib/Algebra/Squarefree/Basic.lean

modified theorem Finset.squarefree_prod_of_pairwise_isCoprime

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Point.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Point.lean

Modified Mathlib/Analysis/InnerProductSpace/Trace.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

modified theorem SimpleGraph.degree_le_card_edgeFinset

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

modified theorem Matrix.PosDef.commute_iff

modified theorem Matrix.PosSemidef.commute_iff

Modified Mathlib/RepresentationTheory/Homological/Resolution.lean

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

modified theorem MvPowerSeries.coeff_prod

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

modified theorem PowerSeries.coeff_prod

Modified Mathlib/RingTheory/TensorProduct/DirectLimitFG.lean

modified theorem TensorProduct.Algebra.exists_of_fg

modified theorem TensorProduct.exists_of_fg

Modified Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean

modified def UniqueFactorizationMonoid.normalizedFactorsEquiv

modified theorem UniqueFactorizationMonoid.normalizedFactorsEquiv_apply

modified theorem UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply

Modified Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean

modified theorem RestrictedProduct.continuous_dom_pi

Modified Mathlib/Topology/Instances/Matrix.lean

modified theorem IsOpen.matrix

Modified Mathlib/Topology/Order/HullKernel.lean

modified theorem PrimitiveSpectrum.closedsGC_closureOperator

modified theorem PrimitiveSpectrum.hull_kernel_of_isClosed

modified theorem PrimitiveSpectrum.isClosed_iff

modified theorem PrimitiveSpectrum.isOpen_iff