Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-04-16 20:12
7bbbee1e
View on Github →
feat(*): various additions to low-level files (
#904
)
feat(*): various additions to low-level files
fix(data/fin): add missing universe
Estimated changes
Modified
src/algebra/order.lean
added
def
decidable.lt_by_cases
Modified
src/data/equiv/basic.lean
added
def
equiv.subtype_congr_right
added
theorem
equiv.subtype_congr_right_mk
Modified
src/data/fin.lean
added
def
{u}
Modified
src/data/nat/basic.lean
added
theorem
nat.add_sub_cancel_right
Modified
src/data/subtype.lean
added
def
subtype.coind
added
theorem
subtype.coind_injective
added
theorem
subtype.map_injective
added
def
subtype.restrict
added
theorem
subtype.restrict_apply
added
theorem
subtype.restrict_def
added
theorem
subtype.restrict_injective
modified
theorem
subtype.val_injective
Modified
src/logic/basic.lean
added
theorem
congr_arg2
Modified
src/logic/embedding.lean
Modified
src/order/basic.lean
added
def
bounded
added
theorem
trans_trichotomous_left
added
theorem
trans_trichotomous_right
added
def
unbounded
Modified
src/order/order_iso.lean
added
theorem
injective_of_increasing
Modified
src/set_theory/cofinality.lean