Commit 2022-12-13 21:37 b040ecc7

View on Github →

feat: port Data.TwoPointing (#984) Mathlib SHA: fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Estimated changes

added theorem TwoPointing.bool_fst
added theorem TwoPointing.bool_snd
added def TwoPointing.pi
added theorem TwoPointing.pi_fst
added theorem TwoPointing.pi_snd
added def TwoPointing.prod
added theorem TwoPointing.prod_fst
added theorem TwoPointing.prod_snd
added theorem TwoPointing.prop_fst
added theorem TwoPointing.prop_snd
added theorem TwoPointing.snd_ne_fst
added theorem TwoPointing.sum_fst
added theorem TwoPointing.sum_snd
added def TwoPointing.swap
added theorem TwoPointing.swap_fst
added theorem TwoPointing.swap_snd
added theorem TwoPointing.swap_swap
added structure TwoPointing