Commit 2024-07-28 19:09 65c21dc1

View on Github →

chore(RingTheory): fix DecidableEq and Fintype vs Finite (#15236)

Estimated changes

Modified Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

modified theorem AdicCompletion.ofTensorProduct_bijective_of_pi_of_fintype

Modified Mathlib/RingTheory/Flat/EquationalCriterion.lean

modified theorem Module.Flat.exists_factorization_of_apply_eq_zero

Modified Mathlib/RingTheory/Idempotents.lean

modified theorem OrthogonalIdempotents.isIdempotentElem_sum

modified theorem OrthogonalIdempotents.lift_of_isNilpotent_ker

modified theorem OrthogonalIdempotents.option

modified theorem OrthogonalIdempotents.surjective_pi