Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-12-14 21:29
79483182
View on Github →
feat(logic/basic): add rewrite rules for nonempty
Estimated changes
Modified
logic/basic.lean
added
theorem
classical.nonempty_pi
added
theorem
nonempty.exists
added
theorem
nonempty.forall
added
theorem
nonempty_Prop
added
theorem
nonempty_empty
added
theorem
nonempty_plift
added
theorem
nonempty_pprod
added
theorem
nonempty_prod
added
theorem
nonempty_psigma
added
theorem
nonempty_psum
added
theorem
nonempty_sigma
added
theorem
nonempty_subtype
added
theorem
nonempty_sum
added
theorem
nonempty_ulift