Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-03-24 09:49
5d242aa4
View on Github →
fix: improve simp lemmas around PartENat.ofENat (
#11553
)
Estimated changes
Modified
Mathlib/Data/Nat/PartENat.lean
added
theorem
PartENat.ofENat_coe
added
theorem
PartENat.ofENat_le
added
theorem
PartENat.ofENat_lt
deleted
theorem
PartENat.ofENat_none
added
theorem
PartENat.ofENat_ofNat
added
theorem
PartENat.ofENat_one
deleted
theorem
PartENat.ofENat_some
added
theorem
PartENat.ofENat_toWithTop
added
theorem
PartENat.ofENat_top
added
theorem
PartENat.ofENat_zero
modified
theorem
PartENat.withTopEquiv_le
modified
theorem
PartENat.withTopEquiv_lt
modified
theorem
PartENat.withTopEquiv_natCast
modified
theorem
PartENat.withTopEquiv_symm_coe
modified
theorem
PartENat.withTopEquiv_symm_one
modified
theorem
PartENat.withTopEquiv_symm_top
modified
theorem
PartENat.withTopEquiv_symm_zero
modified
theorem
PartENat.withTopEquiv_top
Modified
Mathlib/SetTheory/Cardinal/PartENat.lean