Commit 2025-11-03 01:23 6280bdda

View on Github →

feat: extend Equiv.sumCompl API (#30889)

Estimated changes

Modified Mathlib/Logic/Equiv/Fintype.lean

Modified Mathlib/Logic/Equiv/Sum.lean

modified theorem Equiv.sumCompl_apply_inl

modified theorem Equiv.sumCompl_apply_inr

deleted theorem Equiv.sumCompl_apply_symm_of_neg

deleted theorem Equiv.sumCompl_apply_symm_of_pos

added theorem Equiv.sumCompl_symm_apply_neg

added theorem Equiv.sumCompl_symm_apply_of_neg

added theorem Equiv.sumCompl_symm_apply_of_pos

added theorem Equiv.sumCompl_symm_apply_pos