Commit 2024-11-02 17:02 1567c3f4

View on Github →

chore: remove superfluous decidability assumptions (#18553) Cherry-picked from #10235.

Estimated changes

Modified Mathlib/Condensed/Discrete/Colimit.lean

modified def Condensed.fintypeCatAsCofanIsColimit

modified def Condensed.isoFinYonedaComponents

modified theorem Condensed.isoFinYonedaComponents_hom_apply

modified theorem Condensed.isoFinYonedaComponents_inv_comp

modified def LightCondensed.fintypeCatAsCofanIsColimit

modified def LightCondensed.isoFinYonedaComponents

modified theorem LightCondensed.isoFinYonedaComponents_hom_apply

modified theorem LightCondensed.isoFinYonedaComponents_inv_comp

Modified Mathlib/GroupTheory/Perm/DomMulAct.lean

modified theorem DomMulAct.stabilizer_ncard

Modified Mathlib/LinearAlgebra/Matrix/Ideal.lean