Mathlib Changelog
v4
Changelog
About
Github
Commit
2022-12-13 21:37
b040ecc7
View on Github →
feat: port Data.TwoPointing (
#984
) Mathlib SHA: fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/TwoPointing.lean
added
theorem
TwoPointing.bool_fst
added
theorem
TwoPointing.bool_snd
added
theorem
TwoPointing.nonempty_two_pointing_iff
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
theorem
TwoPointing.to_nontrivial
added
structure
TwoPointing