Commit 2025-04-15 17:56 53b9fb34

View on Github →

chore(Fin): fix some @[simp] lemmas (#23967) Some @[simps]-generated lemmas use wrong RHS. Also, one lemma was incorrectly named.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.castAddEmb_apply

added theorem Fin.castSuccEmb_apply

added theorem Fin.coe_castAddEmb

added theorem Fin.coe_succEmb

deleted theorem Fin.val_succEmb

Modified Mathlib/RingTheory/Idempotents.lean