Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-09-29 09:37
0de54327
View on Github →
feat(data/W/cardinal): results about cardinality of W-types (
#9210
)
Estimated changes
Modified
archive/examples/prop_encodable.lean
Renamed
src/data/W.lean
to
src/data/W/basic.lean
added
def
W_type.elim
added
theorem
W_type.elim_injective
added
def
W_type.equiv_sigma
added
theorem
W_type.infinite_of_nonempty_of_is_empty
added
def
W_type.of_sigma
added
theorem
W_type.of_sigma_to_sigma
added
def
W_type.to_sigma
added
theorem
W_type.to_sigma_of_sigma
Created
src/data/W/cardinal.lean
added
theorem
W_type.cardinal_mk_eq_sum
added
theorem
W_type.cardinal_mk_le_max_omega_of_fintype
added
theorem
W_type.cardinal_mk_le_of_le
Modified
src/data/pfunctor/univariate/basic.lean