Theorem Equiv.sumCompl_symm_apply_of_pos

Modification history

2025-11-03 01:23
Mathlib/Logic/Equiv/Sum.lean
feat: extend `Equiv.sumCompl` API (#30889)
Added Equiv.sumCompl_symm_apply_of_posView on Github →