Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-12-11 12:19
be79f9f3
View on Github →
chore(data/cardinal): put embedding into cardinal namespace
Estimated changes
Modified
data/cardinal.lean
added
theorem
cardinal.embedding.antisymm
added
def
cardinal.embedding.arrow_congr_left
added
def
cardinal.embedding.arrow_congr_right
added
theorem
cardinal.embedding.inj'
added
theorem
cardinal.embedding.injective_min
added
def
cardinal.embedding.prod_congr
added
theorem
cardinal.embedding.refl_apply
added
theorem
cardinal.embedding.schroeder_bernstein
added
def
cardinal.embedding.sum_congr
added
theorem
cardinal.embedding.to_fun_eq_coe
added
theorem
cardinal.embedding.total
added
theorem
cardinal.embedding.trans_apply
added
structure
cardinal.embedding
deleted
theorem
embedding.antisymm
deleted
def
embedding.arrow_congr_left
deleted
def
embedding.arrow_congr_right
deleted
theorem
embedding.inj'
deleted
theorem
embedding.injective_min
deleted
def
embedding.prod_congr
deleted
theorem
embedding.refl_apply
deleted
theorem
embedding.schroeder_bernstein
deleted
def
embedding.sum_congr
deleted
theorem
embedding.to_fun_eq_coe
deleted
theorem
embedding.total
deleted
theorem
embedding.trans_apply
deleted
structure
embedding
Modified
data/ordinal.lean